quotientBot — Mathlib

English

The quotient of a ring by the zero ideal is isomorphic to the ring itself.

Русский

Частное кольца от кольца по нулевому идеалу изоморфно самому кольцу.

LaTeX

$$$R/\\{0\\} \\cong R$$$

Lean4

/-- The quotient of a ring by he zero ideal is isomorphic to the ring itself. -/
def quotientBot [Ring R] : R ⧸ (⊥ : Ideal R) ≃+* R :=
  (Ideal.quotEquivOfEq (RingHom.ker_coe_equiv <| .refl _).symm).trans <|
    RingHom.quotientKerEquivOfRightInverse (f := .id R) (g := _root_.id) fun _ ↦ rfl

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