isMaxRank_fundSystem — Mathlib

English

The fundSystem of K has maximal rank: its images under logEmbedding are linearly independent, giving IsMaxRank for fundSystem.

Русский

FundSystem поля K имеет максимальный ранг: изображения через logEmbedding линейно независимы, что даёт IsMaxRank для fundSystem.

LaTeX

$$IsMaxRank (fundSystem K)$$

Lean4

theorem isMaxRank_fundSystem : IsMaxRank (fundSystem K) := by
  classical
  convert ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent
  rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]

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