kerLift_mk — Mathlib

English

When the congruence is the kernel of f, the kerLift evaluated at x equals f x; i.e., kerLift f x = f x.

Русский

Если конгруэнция является ядром f, то kerLift f x = f x.

LaTeX

$$$\kerLift f x = f x$$$

Lean4

/-- The diagram described by the universal property for quotients of monoids, when the congruence
relation is the kernel of the homomorphism, commutes. -/
@[to_additive (attr := simp) /-- The diagram described by the universal property for quotients
    of `AddMonoid`s, when the additive congruence relation is the kernel of the homomorphism,
    commutes. -/
    ]
theorem kerLift_mk (x : M) : kerLift f x = f x :=
  rfl

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