English
The finite type Fin n carries a commutative semigroup structure under multiplication.
Русский
Конечный тип Fin n обладает когомонной полугруппой под умножением.
LaTeX
$$$\text{CommSemigroup}(\text{Fin } n)$$$
Lean4
/-- Multiplicative commutative semigroup structure on `Fin n`. -/
instance instCommSemigroup (n : ℕ) : CommSemigroup (Fin n) :=
{
inferInstanceAs
(Mul (Fin n)) with
mul_assoc := fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
Fin.eq_of_val_eq <|
calc
a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
_ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
_ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
mul_comm := Fin.mul_comm }
