d_map — Mathlib

English

If f: A → B is a ring homomorphism and D is a derivation on B with respect to an A-algebra structure, then D composed with f vanishes on the image of A, i.e., D(f(a)) = 0 for all a ∈ A.

Русский

Если f: A → B — кольцевой однородный гомоморфизм и D — производная на B относительно структуры по A, то D(f(a)) = 0 для всех a ∈ A.

LaTeX

$$$\\forall a \\in A:\\; D.d (f(a)) = 0.$$$

Lean4

@[simp]
theorem d_map (a : A) : D.d (f a) = 0 :=
  letI := f.hom.toAlgebra
  letI := Module.compHom M f.hom
  D.map_algebraMap a

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