Monoid.ext
theorem Monoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : Monoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
The theorem `Monoid.ext` states that for any type `M`, if there are two monoid instances `m₁` and `m₂` on `M` such that their multiplication operations `HMul.hMul` (which computes the product of two elements) are equal, then the two monoid instances `m₁` and `m₂` are indeed the same. Essentially, this theorem is saying that the multiplication operation determines a monoid structure.
More concisely: If two monoid structures on a type have equal multiplication operations, then they are equal.
|
AddMonoid.ext
theorem AddMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : AddMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
The theorem `AddMonoid.ext` states that for any type `M`, if `m₁` and `m₂` are two additive monoids on `M` such that their addition operations (`HAdd.hAdd`) are equivalent, then `m₁` and `m₂` must be the same additive monoid. In other words, this theorem asserts the uniqueness of the additive monoid structure on `M` in terms of its addition operation.
More concisely: If two additive monoids on a type `M` have equivalent addition operations, then they are equal.
|