LeanPool.BruhatTits.Utils.GLSubmoduleAction

theorem BruhatTits.scalar_smul_GL_smul {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Submodule (↥R) (ι → K)) (a : K) (g : GL ι K) : a • g • M = g • a • M

theorem BruhatTits.smul_GL_mono {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {M L : Submodule (↥R) (ι → K)} (g : GL ι K) (hML : M ≤ L) : g • M ≤ g • L

theorem BruhatTits.smul_le_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {M L : Submodule (↥R) (ι → K)} (g : GL ι K) : g • M ≤ g • L ↔ M ≤ L

theorem BruhatTits.smul_eq_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (g : GL ι K) (M L : Submodule (↥R) (ι → K)) : g • M = g • L ↔ M = L

theorem BruhatTits.smul_lt_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (g : GL ι K) (M L : Submodule (↥R) (ι → K)) : g • M < g • L ↔ M < L