associated_left_inverse' — Mathlib

English

A version of associated_isSymm for general targets: flip of associatedHom equals associatedHom.

Русский

Версия associated_isSymm для общих целей: flip associatedHom равен associatedHom.

LaTeX

$$$ associated_flip : (associatedHom S Q).flip = associatedHom S Q $$$

Lean4

/-- A version of `QuadraticMap.associated_left_inverse` for general targets. -/
theorem associated_left_inverse' {B₁ : BilinMap R M N} (hB₁ : B₁.flip = B₁) : associatedHom S B₁.toQuadraticMap = B₁ :=
  by
  ext _ y
  rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]

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