------------------------------------------------------------------------
-- The Agda standard library
--
-- Multiplication over a monoid (i.e. repeated addition)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (CommutativeMonoid)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
module Algebra.Properties.CommutativeMonoid.Mult
{a ℓ} (M : CommutativeMonoid a ℓ) where
-- View of the monoid operator as addition
open CommutativeMonoid M
renaming
( _∙_ to _+_
; ∙-cong to +-cong
; ∙-congʳ to +-congʳ
; ∙-congˡ to +-congˡ
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
; assoc to +-assoc
; ε to 0#
)
open import Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
------------------------------------------------------------------------
-- Re-export definition and properties for monoids
open import Algebra.Properties.Monoid.Mult monoid public
------------------------------------------------------------------------
-- Properties of _×_
×-distrib-+ : ∀ x y n → n × (x + y) ≈ n × x + n × y
×-distrib-+ x y zero = sym (+-identityˡ 0# )
×-distrib-+ x y (suc n) = begin
x + y + n × (x + y) ≈⟨ +-congˡ (×-distrib-+ x y n) ⟩
x + y + (n × x + n × y) ≈⟨ +-assoc x y (n × x + n × y) ⟩
x + (y + (n × x + n × y)) ≈⟨ +-congˡ (x∙yz≈y∙xz y (n × x) (n × y)) ⟩
x + (n × x + suc n × y) ≈⟨ x∙yz≈xy∙z x (n × x) (suc n × y) ⟩
suc n × x + suc n × y ∎
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