val_smul''' — Mathlib

English

If ker is finitely generated, then the cotangent space is finite over S.

Русский

Если ядро порождено конечным числом элементов, котангентовое пространство над S конечномерно.

LaTeX

$$$$ P.ker.FG \to M \implies M = P.Cotangent \text{ is finite over } S $$$$

Lean4

/-- The action of `R₀` on `P.Cotangent` for an extension `P → S`, if `S` is an `R₀` algebra. -/
theorem val_smul''' {R₀} [CommRing R₀] [Algebra R₀ S] (r : R₀) (x : P.Cotangent) :
    (r • x).val = P.σ (algebraMap R₀ S r) • x.val :=
  rfl

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