polarBilin_injective — Mathlib

English

If 2 is a unit in R, the map polarBilin: QuadraticMap R M N → BilinMap R M N is injective.

Русский

Если 2 является единицей в R, отображение polarBilin: QuadraticMap R M N → BilinMap R M N инъективно.

LaTeX

$$$ (\forall h: IsUnit(2:R),\; polarBilin: QuadraticMap R M N \to _ \text{ is injective }) $$$

Lean4

theorem _root_.QuadraticMap.polarBilin_injective (h : IsUnit (2 : R)) :
    Function.Injective (polarBilin : QuadraticMap R M N → _) :=
  by
  intro Q₁ Q₂ h₁₂
  apply h.smul_left_cancel.mp
  rw [show (2 : R) = (2 : ℕ) by rfl]
  simp_rw [Nat.cast_smul_eq_nsmul R, ← QuadraticMap.toQuadraticMap_polarBilin]
  exact congrArg toQuadraticMap h₁₂

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