val_smul'' — Mathlib

English

The value of the quotient map mk applied to an element of the kernel equals the cotangent element associated to that kernel element.

Русский

Значение отображения mk, применённого к элементу ядра, равно соответствующему котангентовому элементу, ассоциированному с этим элементом ядра.

LaTeX

$$$$ (mk x).val = Ideal.toCotangent ~ x $$$$

Lean4

/-- The action of `R` on `P.Cotangent` for an `R`-extension `P → S`. -/
@[simp]
theorem val_smul'' (r : R) (x : P.Cotangent) : (r • x).val = r • x.val := by
  rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]

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