    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Multiplication over a semiring optimised for type-checking.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra
    open import Data.Nat.Base as ℕ using (zero; suc)

    module Algebra.Properties.Semiring.Mult.TCOptimised
      {a ℓ} (S : Semiring a ℓ) where

    open Semiring S renaming (zero to *-zero)
    open import Relation.Binary.Reasoning.Setoid setoid

    open import Algebra.Properties.Semiring.Mult S as U
      using () renaming (_×_ to _×ᵤ_)

    ------------------------------------------------------------------------
    -- Re-export definition from the monoid

    open import Algebra.Properties.Monoid.Mult.TCOptimised +-monoid public

    ------------------------------------------------------------------------
    -- Properties of _×_

    -- (_×′ 1#) is homomorphic with respect to _ℕ.*_/_*_.

    ×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
    ×1-homo-* m n = begin
      (m ℕ.* n) ×  1#        ≈⟨ ×ᵤ≈× (m ℕ.* n) 1# ⟨
      (m ℕ.* n) ×ᵤ 1#        ≈⟨  U.×1-homo-* m n ⟩
      (m ×ᵤ 1#) * (n ×ᵤ 1#)  ≈⟨  *-cong (×ᵤ≈× m 1#) (×ᵤ≈× n 1#) ⟩
      (m ×  1#) * (n ×  1#)  ∎