two_nsmul_associated — Mathlib

English

An explicit construction showing that if 2 is invertible in R, then the endomorphism 2 on M is invertible with the expected inverse.

Русский

Явное построение: если 2 обращаемо в R, тогда 2 на M обращаемо и обратное соответствует ожидаемому.

LaTeX

$$$ \text{Invertible }(2 : \mathrm{End}_R(M)) $$$

Lean4

/-- Twice the associated bilinear map of `Q` is the same as the polar of `Q`. -/
@[simp]
theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin :=
  by
  ext
  dsimp
  rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply, polar]

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