Theorems · Theorem · linear algebra

LinearMap.finrank_le_of_isSMulRegular

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {S : Type u_2} [inst_4 : CommSemiring S] [inst_5 : Algebra S R] [inst_6 : Module S M] [IsScalarTower S R M]
  (L L' : Submodule R M) [Module.Finite R ↥L'] {s : S},
  IsSMulRegular M s → (∀ x ∈ L, s • x ∈ L') → Module.finrank R ↥L ≤ Module.finrank R ↥L'

Defined in

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleStrongRankConditionCommSemiringAlgebraModuleIsScalarTowerModule.Finite