polar_smul_right_of_tower — Mathlib

English

An alternative constructor to QuadraticMap.mk exists, using polar to define Q via toFun and polar-related laws.

Русский

Существуют альтернативные конструкторы QuadraticMap.mk, использующие polar для определения Q через свойства polar.

LaTeX

$$def ofPolar (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x) (polar_add_left : ∀ x x' y : M, polar toFun (x + x') y = polar toFun x y + polar toFun x' y) (polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y) : QuadraticMap R M N$$

Lean4

@[simp]
theorem polar_smul_right_of_tower (a : S) (x y : M) : polar Q x (a • y) = a • polar Q x y := by
  rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]

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