coe_mul — Mathlib

English

The quotient map commutes with multiplication: Con.toQuotient (x y) = Con.toQuotient x · Con.toQuotient y.

Русский

Коэффициентная карта сохраняет умножение: Con.toQuotient( x y ) = Con.toQuotient x · Con.toQuotient y.

LaTeX

$$$Con.toQuotient (x\\,y) = Con.toQuotient x \\; \\cdot \\; Con.toQuotient y$$$

Lean4

/-- The coercion to the quotient of a congruence relation commutes with multiplication (by
definition). -/
@[to_additive (attr := simp) /-- The coercion to the quotient of an additive congruence relation
    commutes with addition (by definition). -/
    ]
theorem coe_mul (x y : M) : (↑(x * y) : c.Quotient) = ↑x * ↑y :=
  rfl

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