coe_one — Mathlib

English

In the quotient by a monoid, the unit element is represented by the class of 1.

Русский

В фактор-группе по моноиду единица задаётся классом единицы в моноиде.

LaTeX

$$$1_{c} = 1$$$

Lean4

/-- The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the
monoid's 1. -/
@[to_additive (attr := simp) /-- The 0 of the quotient of an `AddMonoid` by an additive congruence
    relation is the equivalence class of the `AddMonoid`'s 0. -/
    ]
theorem coe_one : ((1 : M) : c.Quotient) = 1 :=
  rfl

Похожие утверждения