------------------------------------------------------------------------
-- The Agda standard library
--
-- Multiplication by a natural number over a semiring
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Semiring)
module Algebra.Properties.Semiring.Mult
{a ℓ} (S : Semiring a ℓ) where
open import Data.Nat.Base as ℕ using (zero; suc)
open Semiring S renaming (zero to *-zero)
open import Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Definitions _≈_ using (_IdempotentOn_)
------------------------------------------------------------------------
-- Re-export definition from the monoid
open import Algebra.Properties.Monoid.Mult +-monoid public
------------------------------------------------------------------------
-- Properties of _×_
-- (0 ×_) is (0# *_)
×-homo-0# : ∀ x → 0 × x ≈ 0# * x
×-homo-0# x = sym (zeroˡ x)
-- (1 ×_) is (1# *_)
×-homo-1# : ∀ x → 1 × x ≈ 1# * x
×-homo-1# x = trans (×-homo-1 x) (sym (*-identityˡ x))
-- (n ×_) commutes with _*_
×-comm-* : ∀ n x y → x * (n × y) ≈ n × (x * y)
×-comm-* zero x y = zeroʳ x
×-comm-* (suc n) x y = begin
x * (suc n × y) ≡⟨⟩
x * (y + n × y) ≈⟨ distribˡ _ _ _ ⟩
x * y + x * (n × y) ≈⟨ +-congˡ (×-comm-* n _ _) ⟩
x * y + n × (x * y) ≡⟨⟩
suc n × (x * y) ∎
-- (n ×_) associates with _*_
×-assoc-* : ∀ n x y → (n × x) * y ≈ n × (x * y)
×-assoc-* zero x y = zeroˡ y
×-assoc-* (suc n) x y = begin
(suc n × x) * y ≡⟨⟩
(x + n × x) * y ≈⟨ distribʳ _ _ _ ⟩
x * y + (n × x) * y ≈⟨ +-congˡ (×-assoc-* n _ _) ⟩
x * y + n × (x * y) ≡⟨⟩
suc n × (x * y) ∎
-- (_× x) is homomorphic with respect to _ℕ.*_/_*_ for idempotent x.
idem-×-homo-* : ∀ m n {x} → (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
idem-×-homo-* m n {x} idem = begin
(m × x) * (n × x) ≈⟨ ×-assoc-* m x (n × x) ⟩
m × (x * (n × x)) ≈⟨ ×-congʳ m (×-comm-* n x x) ⟩
m × (n × (x * x)) ≈⟨ ×-assocˡ _ m n ⟩
(m ℕ.* n) × (x * x) ≈⟨ ×-congʳ (m ℕ.* n) idem ⟩
(m ℕ.* n) × x ∎
-- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_.
×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
×1-homo-* m n = sym (idem-×-homo-* m n (*-identityʳ 1#))
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.1
1×-identityʳ = ×-homo-1
{-# WARNING_ON_USAGE 1×-identityʳ
"Warning: 1×-identityʳ was deprecated in v2.1.
Please use ×-homo-1 instead. "
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4