algebraMap_posForm — Mathlib

English

Congruence lemma: if two RootPositiveForm objects are equal, then their associated posForm coincide after transporting scalars.

Русский

Лемма эквивалентности: если два RootPositiveForm равны, то их posForm совпадают после переноса скаляров.

LaTeX

$$$ B.toInvariantForm = B_1.toInvariantForm \\Rightarrow B.posForm = B_1.posForm $$$

Lean4

@[simp]
theorem algebraMap_posForm {x y : span S (range P.root)} : algebraMap S R (B.posForm x y) = B.form x y :=
  by
  change Algebra.linearMap S R _ = _
  simp [posForm]

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