realSpaceToLogSpace_completeFamily_of_eq

English

For i with i ≠ w0, realSpaceToLogSpace(completeFamily i) equals basisUnitLattice at equivFinRank.symm i.

Русский

Для i ≠ w0: realSpaceToLogSpace(completeFamily(i)) = basisUnitLattice( K)(equivFinRank.symm i).

LaTeX

$$$\text{realSpaceToLogSpace}(\text{completeFamily}(i)) = \text{basisUnitLattice}(K)(\text{equivFinRank}^{-1}(i))$ for i ≠ w0$$

Lean4

theorem realSpaceToLogSpace_completeFamily_of_eq : realSpaceToLogSpace (completeFamily K w₀) = 0 :=
  by
  ext
  rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]

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