ringQuot_ext' — Mathlib

English

The extensionality lemma for AlgHoms from RingQuot via mkAlgHom.

Русский

Лемма экстенсиональности для AlgHom из RingQuot через mkAlgHom.

LaTeX

$$$\\text{ringQuot_ext'}$ — Extensionality for AlgHom via mkAlgHom。$$

Lean4

@[ext 1100]
theorem ringQuot_ext' {s : A → A → Prop} (f g : RingQuot s →ₐ[S] B)
    (w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)) : f = g :=
  by
  ext x
  rcases mkAlgHom_surjective S s x with ⟨x, rfl⟩
  exact AlgHom.congr_fun w x

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