ringQuotToIdealQuotient_apply — Mathlib

English

The same statement as 33544, expressed with the explicit target as an Ideal quotient.

Русский

То же самое, что и в 33544, выраженное через косвенный объект через идеальный квот.

LaTeX

$$$ringQuotToIdealQuotient\\ r\\ (mkRingHom\\ r\\ x) = Ideal.Quotient.mk (Ideal.ofRel r)\\ x$$$

Lean4

@[simp]
theorem ringQuotToIdealQuotient_apply (r : B → B → Prop) (x : B) :
    ringQuotToIdealQuotient r (mkRingHom r x) = Ideal.Quotient.mk (Ideal.ofRel r) x :=
  by
  simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]
  rfl

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