val_smul' — Mathlib

English

The cotangent map of the identity is the identity map on cotangent spaces.

Русский

Котангентово отображение тождества является тождественным отображением на котангентовых пространствах.

LaTeX

$$$$ \mathrm{Cotangent}.map (\mathrm{id~P}) = \mathrm{LinearMap.id} $$$$

Lean4

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

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