dotProduct_star_self_pos_iff — Mathlib

English

0 < dotProduct v star(v) iff v ≠ 0.

Русский

0 < dotProduct v star(v) тогда и только если v ≠ 0.

LaTeX

$$0 < \langle v, v^* \rangle \iff v \neq 0$$

Lean4

/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`. -/
@[simp]
theorem dotProduct_star_self_pos_iff {v : n → R} : 0 < star v ⬝ᵥ v ↔ v ≠ 0 :=
  by
  nontriviality R
  refine (Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_
  simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]
  refine (and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_
  constructor
  · rintro h hv
    simp [hv] at h
  · exact (star_mul_self_pos <| isRegular_of_ne_zero ·)

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