IsMaxRank — Mathlib

English

An abbreviation: IsMaxRank(u) holds when the family u of units attains maximal rank, i.e., its log-embeddings are linearly independent over the reals.

Русский

Утверждение IsMaxRank(u) означает, что семейство единиц достигает максимального ранга, то есть вектор изображений через лог-вплотения линейно независим над вещественными числами.

LaTeX

$$$\\text{IsMaxRank}(u) :\\iff\\text{LinearIndependent}_{\\mathbb{R}}(\\lambda i \\mapsto \\logEmbedding(K, Additive.ofMul(u_i))).$$$

Lean4

/-- A family of units is of maximal rank if its image by `logEmbedding` is linearly independent
over `ℝ`.
-/
abbrev IsMaxRank (u : Fin (rank K) → (𝓞 K)ˣ) : Prop :=
  LinearIndependent ℝ (fun i ↦ logEmbedding K (Additive.ofMul (u i)))

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