factor — Mathlib

English

mk I a = 0 iff a ∈ I.

Русский

mk I a = 0 эквивалентно a ∈ I.

LaTeX

$$$mk_I(a) = 0 \\iff a \\in I$$$

Lean4

/-- The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.

This is the `Ideal.Quotient` version of `Quot.Factor`

When the two ideals are of the form `I^m` and `I^n` and `n ≤ m`,
please refer to the dedicated version `Ideal.Quotient.factorPow`. -/
def factor (H : S ≤ T) : R ⧸ S →+* R ⧸ T :=
  Ideal.Quotient.lift S (mk T) fun _ hx => eq_zero_iff_mem.2 (H hx)

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