English
Simplification lemma showing that anisotropy equivalence can be tested componentwise.
Русский
Смягчающая лемма, показывающая тестирование анизотропии по компонентам.
LaTeX
$$$ (\\pi Q).Anisotropic \\Rightarrow \\forall i, Q_i.Anisotropic. $$$
Lean4
/-- If a family is anisotropic then its components must be. The converse is not true. -/
theorem anisotropic_of_pi [Fintype ι] {Q : ∀ i, QuadraticMap R (Mᵢ i) P} (h : (pi Q).Anisotropic) :
∀ i, (Q i).Anisotropic :=
by
simp_rw [Anisotropic, pi_apply, funext_iff, Pi.zero_apply] at h
intro i x hx
classical
have := h (Pi.single i x) ?_ i
· rw [Pi.single_eq_same] at this
exact this
apply Finset.sum_eq_zero
intro j _
by_cases hji : j = i
· subst hji; rw [Pi.single_eq_same, hx]
· rw [Pi.single_eq_of_ne hji, map_zero]
