IterateMapComap

📁 Source: Mathlib/Algebra/Module/Submodule/IterateMapComap.lean

Statistics

Metric	Count
Definitions iterateMapComap	1
Theorems iterateMapComap_eq_succ, iterateMapComap_le_succ, ker_le_of_iterateMapComap_eq_succ	3
Total	4

LinearMap

Definitions

Name	Category	Theorems
iterateMapComap 📖	CompOp	1 math math: iterateMapComap_le_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iterateMapComap_eq_succ 📖	—	iterateMapComap DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—	Mathlib.Tactic.Contrapose.contrapose₁ RingHomSurjective.ids iterateMapComap.eq_1 Function.iterate_succ' Submodule.map_injective_of_injective Submodule.comap_injective_of_surjective
iterateMapComap_le_succ 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	iterateMapComap	—	RingHomSurjective.ids iterateMapComap.eq_1 Function.iterate_succ' Submodule.map_le_iff_le_comap Submodule.map.congr_simp Submodule.map_comap_le le_imp_le_of_le_of_le le_refl Submodule.map_mono Submodule.le_comap_map Submodule.comap_mono
ker_le_of_iterateMapComap_eq_succ 📖	mathematical	iterateMapComap DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ker	—	iterateMapComap_eq_succ ker_le_comap RingHomSurjective.ids

---

← Back to Index