English
Let S be a module-finite free R-algebra; for a nonzero R-free left ideal I of S, the R-rank of I equals the rank of S.
Русский
Пусть S — модульно конечная свободная R-алгебра; для ненулевого правого идеала I модуля S ранги по R совпадают: rank_R(I) = rank_R(S).
LaTeX
$$Fintype.card m = Fintype.card n$$
Lean4
/-- An induction (and recursion) principle for proving results about all submodules of a fixed
finite free module `M`. A property is true for all submodules of `M` if it satisfies the following
"inductive step": the property is true for a submodule `N` if it's true for all submodules `N'`
of `N` with the property that there exists `0 ≠ x ∈ N` such that the sum `N' + Rx` is direct. -/
def inductionOnRank {R M} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] [IsDomain R] [Finite ι]
(b : Basis ι R M) (P : Submodule R M → Sort*)
(ih : ∀ N : Submodule R M, (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N)
(N : Submodule R M) : P N :=
letI := Fintype.ofFinite ι
Submodule.inductionOnRankAux b P ih (Fintype.card ι) N fun hs hli => by
simpa using b.card_le_card_of_linearIndependent hli
