liftOfDerivationToSquareZero_mk_apply'

English

If d: Derivation R A I and x ∈ A, then (d x) plus the canonical image of x in B/I equals the canonical image of x in B/I.

Русский

Если d: Derivation R A I и x ∈ A, то d x + algebraMap_A(B/I)(x) = algebraMap_A(B/I)(x).

LaTeX

$$$(Ideal.Quotient.mk I)(d x) + (algebraMap A (B/I)) x = algebraMap A (B/I) x$$$

Lean4

@[simp]
theorem liftOfDerivationToSquareZero_mk_apply' (d : Derivation R A I) (x : A) :
    (Ideal.Quotient.mk I) (d x) + (algebraMap A (B ⧸ I)) x = algebraMap A (B ⧸ I) x := by
  simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]

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