Theorems · Theorem · commutative algebra

LinearMap.iterateMapComap_le_succ

∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N),
  Submodule.map f K ≤ Submodule.map i K → ∀ (n : ℕ), f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

If f(K) ≤ i(K), then LinearMap.iterateMapComap is not decreasing.

Defined in

Mathlib.Algebra.Module.Submodule.IterateMapComap

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule