polarization_apply_eq_zero_iff — Mathlib

English

Polarization annihilates an element m if and only if RootForm annihilates m: P.Polarization m = 0 ⇔ P.RootForm m = 0.

Русский

Поляризация аннигилирует элемент m тогда и только тогда, когда RootForm аннигилирует m: P.Polarization m = 0 ⇔ P.RootForm m = 0.

LaTeX

$$$ P.Polarization(m) = 0 \\iff P.RootForm(m) = 0 $$$

Lean4

theorem polarization_apply_eq_zero_iff (m : M) : P.Polarization m = 0 ↔ P.RootForm m = 0 :=
  by
  rw [← flip_comp_polarization_eq_rootForm]
  refine ⟨fun h ↦ by simp [h], ?_⟩
  rintro (h : P.flip.toPerfPair (P.Polarization m) = 0)
  simpa only [EmbeddingLike.map_eq_zero_iff] using h

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