Loogle!
Result
Found 368 declarations mentioning Submodule.map. Of these, only the first 200 are shown.
- Submodule.map 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : Submodule R₂ M₂ - Submodule.map_injective_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (Submodule.map f) - Submodule.map_surjective_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) : Function.Surjective (Submodule.map f) - Submodule.map_id 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.map LinearMap.id p = p - Submodule.map_bot 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : Submodule.map f ⊥ = ⊥ - Submodule.comap_map_eq_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) (p : Submodule R M) : Submodule.comap f (Submodule.map f p) = p - Submodule.map_comap_eq_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) (p : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p) = p - Submodule.map_coe 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : ↑(Submodule.map f p) = ⇑f '' ↑p - Submodule.map_eq_bot_iff 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} : Submodule.map e p = ⊥ ↔ p = ⊥ - Submodule.map_eq_top_iff 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} : Submodule.map e p = ⊤ ↔ p = ⊤ - Submodule.map_ne_bot_iff 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} : Submodule.map e p ≠ ⊥ ↔ p ≠ ⊥ - Submodule.map_ne_top_iff 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} : Submodule.map e p ≠ ⊤ ↔ p ≠ ⊤ - Submodule.range_map_nonempty 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (N : Submodule R M) : (Set.range fun ϕ => Submodule.map ϕ N).Nonempty - Submodule.mem_map_of_mem 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {r : M} (h : r ∈ p) : f r ∈ Submodule.map f p - Submodule.le_comap_map 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (p : Submodule R M) : p ≤ Submodule.comap f (Submodule.map f p) - Submodule.map_comap_le 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f q) ≤ q - Submodule.mem_map 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂} : x ∈ Submodule.map f p ↔ ∃ y ∈ p, f y = x - Submodule.comap_iInf_map_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) {ι : Sort u_10} (S : ι → Submodule R M) : Submodule.comap f (⨅ i, Submodule.map f (S i)) = iInf S - Submodule.map_iInf_comap_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) {ι : Sort u_10} (S : ι → Submodule R₂ M₂) : Submodule.map f (⨅ i, Submodule.comap f (S i)) = iInf S - Submodule.map_strictMono_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) : StrictMono (Submodule.map f) - Submodule.map_iInf 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {ι : Sort u_10} [Nonempty ι] {p : ι → Submodule R M} (f : F) (hf : Function.Injective ⇑f) : Submodule.map f (⨅ i, p i) = ⨅ i, Submodule.map f (p i) - Submodule.map_zero 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R M) [RingHomSurjective σ₁₂] : Submodule.map 0 p = ⊥ - Submodule.map_coe_toLinearMap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : Submodule.map (↑f) p = Submodule.map f p - Submodule.map_inf_eq_map_inf_comap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {p' : Submodule R₂ M₂} : Submodule.map f p ⊓ p' = Submodule.map f (p ⊓ Submodule.comap f p') - Submodule.gc_map_comap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : GaloisConnection (Submodule.map f) (Submodule.comap f) - Submodule.apply_coe_mem_map 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : Submodule R M} (r : ↥p) : f ↑r ∈ Submodule.map f p - Submodule.map_inf_comap_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) (p q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p ⊓ Submodule.comap f q) = p ⊓ q - Submodule.comap_inf_map_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) (p q : Submodule R M) : Submodule.comap f (Submodule.map f p ⊓ Submodule.map f q) = p ⊓ q - Submodule.gciMapComap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) : GaloisCoinsertion (Submodule.map f) (Submodule.comap f) - Submodule.giMapComap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) : GaloisInsertion (Submodule.map f) (Submodule.comap f) - Submodule.map_inf 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p q : Submodule R M} (hf : Function.Injective ⇑f) : Submodule.map f (p ⊓ q) = Submodule.map f p ⊓ Submodule.map f q - Submodule.map_iSup 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {ι : Sort u_10} (f : F) (p : ι → Submodule R M) : Submodule.map f (⨆ i, p i) = ⨆ i, Submodule.map f (p i) - Submodule.comap_iSup_map_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) {ι : Sort u_10} (S : ι → Submodule R M) : Submodule.comap f (⨆ i, Submodule.map f (S i)) = iSup S - Submodule.map_iSup_comap_of_sujective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) {ι : Sort u_10} (S : ι → Submodule R₂ M₂) : Submodule.map f (⨆ i, Submodule.comap f (S i)) = iSup S - Submodule.map_iSup_comap_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) {ι : Sort u_10} (S : ι → Submodule R₂ M₂) : Submodule.map f (⨆ i, Submodule.comap f (S i)) = iSup S - Submodule.map_le_iff_le_comap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} : Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q - Submodule.map_mono 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p p' : Submodule R M} : p ≤ p' → Submodule.map f p ≤ Submodule.map f p' - Submodule.map_inf_le 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p q : Submodule R M} : Submodule.map f (p ⊓ q) ≤ Submodule.map f p ⊓ Submodule.map f q - Submodule.comap_lt_of_lt_map_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) {p : Submodule R M} {q : Submodule R₂ M₂} (h : q < Submodule.map f p) : Submodule.comap f q < p - Submodule.le_map_of_comap_le_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} {q : Submodule R₂ M₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) (h : Submodule.comap f q ≤ p) : q ≤ Submodule.map f p - Submodule.lt_map_of_comap_lt_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {p : Submodule R M} {q : Submodule R₂ M₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) (h : Submodule.comap f q < p) : q < Submodule.map f p - Submodule.map_covBy_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) {p q : Submodule R M} (h : p ⋖ q) : Submodule.map f p ⋖ Submodule.map f q - Submodule.map_le_map_iff_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) (p q : Submodule R M) : Submodule.map f p ≤ Submodule.map f q ↔ p ≤ q - Submodule.map_lt_map_iff_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) {p q : Submodule R M} : Submodule.map f p < Submodule.map f q ↔ p < q - Submodule.map.congr_simp 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ σ₁₂✝ : R →+* R₂} (e_σ₁₂ : σ₁₂ = σ₁₂✝) [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f f✝ : F) (e_f : f = f✝) (p p✝ : Submodule R M) (e_p : p = p✝) : Submodule.map f p = Submodule.map f✝ p✝ - Submodule.map_sup 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p p' : Submodule R M) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) : Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p' - Submodule.map_sup_comap_of_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective ⇑f) (p q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f p ⊔ Submodule.comap f q) = p ⊔ q - Submodule.comap_sup_map_of_injective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective ⇑f) (p q : Submodule R M) : Submodule.comap f (Submodule.map f p ⊔ Submodule.map f q) = p ⊔ q - LinearEquiv.map_eq_comap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) : Submodule.map (↑e) K = Submodule.comap (↑e.symm) K - Submodule.comap_equiv_eq_map_symm 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂) : Submodule.comap (↑e) K = Submodule.map (↑e.symm) K - Submodule.map_equiv_eq_comap_symm 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) : Submodule.map (↑e) K = Submodule.comap (↑e.symm) K - Submodule.equivMapOfInjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) : ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map f p) - Submodule.mem_map_equiv 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (p : Submodule R M) {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ Submodule.map (↑e) p ↔ e.symm x ∈ p - Submodule.map_toAddSubmonoid' 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid - Submodule.map_comp 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R M) : Submodule.map (g ∘ₛₗ f) p = Submodule.map g (Submodule.map f p) - LinearMap.submoduleMap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) : ↥p →ₗ[R] ↥(Submodule.map f p) - Submodule.map_neg 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) : Submodule.map (-f) p = Submodule.map f p - Submodule.map_toAddSubmonoid 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (↑f) p.toAddSubmonoid - Submodule.map_add_le 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R M) [RingHomSurjective σ₁₂] (f g : M →ₛₗ[σ₁₂] M₂) : Submodule.map (f + g) p ≤ Submodule.map f p ⊔ Submodule.map g p - Submodule.map_symm_eq_iff 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {p : Submodule R M} (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} : Submodule.map e.symm K = p ↔ Submodule.map e p = K - Submodule.orderIsoMapComap_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) : (Submodule.orderIsoMapComap f) p = Submodule.map f p - LinearEquiv.submoduleMap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) : ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map (↑e) p) - Submodule.orderIsoMapComapOfBijective_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Function.Bijective ⇑f) (p : Submodule R M) : (Submodule.orderIsoMapComapOfBijective f hf) p = Submodule.map f p - Submodule.map_comap_subtype 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) : Submodule.map p.subtype (Submodule.comap p.subtype p') = p ⊓ p' - Submodule.map_smul 📋 Mathlib.Algebra.Module.Submodule.Map
{K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) (h : a ≠ 0) : Submodule.map (a • f) p = Submodule.map f p - Submodule.map_toAddSubgroup 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M) : (Submodule.map f p).toAddSubgroup = AddSubgroup.map (↑f) p.toAddSubgroup - Submodule.map_smul' 📋 Mathlib.Algebra.Module.Submodule.Map
{K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) : Submodule.map (a • f) p = ⨆ (_ : a ≠ 0), Submodule.map f p - Submodule.orderIsoMapComap_symm_apply' 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) : (Submodule.orderIsoMapComap e).symm p = Submodule.map e.symm p - LinearMap.comap_codRestrict 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p) (p' : Submodule R ↥p) : Submodule.comap (LinearMap.codRestrict p f hf) p' = Submodule.comap f (Submodule.map p.subtype p') - LinearMap.map_codRestrict 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c ∈ p) (p' : Submodule R₂ M₂) : Submodule.map (LinearMap.codRestrict p f h) p' = Submodule.comap p.subtype (Submodule.map f p') - AddMonoidHom.coe_toIntLinearMap_map 📋 Mathlib.Algebra.Module.Submodule.Map
{A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A) : Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s) - Submodule.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥p) : ↑((Submodule.equivMapOfInjective f i p) x) = f ↑x - LinearMap.submoduleMap_surjective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) : Function.Surjective ⇑(f.submoduleMap p) - LinearMap.submoduleMap_coe_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} (x : ↥p) : ↑((f.submoduleMap p) x) = f ↑x - Submodule.map_equivMapOfInjective_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥(Submodule.map f p)) : f ↑((Submodule.equivMapOfInjective f i p).symm x) = ↑x - LinearEquiv.submoduleMap_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥p) : ↑((e.submoduleMap p) x) = e ↑x - LinearEquiv.submoduleMap_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : ↥(Submodule.map (↑e) p)) : ↑((e.submoduleMap p).symm x) = e.symm ↑x - LinearMap.le_ker_iff_map 📋 Mathlib.Algebra.Module.Submodule.Ker
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : p ≤ LinearMap.ker f ↔ Submodule.map f p = ⊥ - LinearMap.range_eq_map 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : LinearMap.range f = Submodule.map f ⊤ - Submodule.map_top 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : Submodule.map f ⊤ = LinearMap.range f - Submodule.map_comap_eq 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) : Submodule.map f (Submodule.comap f q) = LinearMap.range f ⊓ q - LinearMap.map_le_range 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : Submodule.map f p ≤ LinearMap.range f - Submodule.map_comap_eq_of_le 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} (h : p ≤ LinearMap.range f) : Submodule.map f (Submodule.comap f p) = p - Submodule.map_comap_eq_self 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂} (h : q ≤ LinearMap.range f) : Submodule.map f (Submodule.comap f q) = q - LinearMap.range_comp 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : LinearMap.range (g ∘ₛₗ f) = Submodule.map g (LinearMap.range f) - Submodule.map_subtype_le 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R ↥p) : Submodule.map p.subtype p' ≤ p - Submodule.map_subtype_top 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.map p.subtype ⊤ = p - LinearMap.range_domRestrict 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (K : Submodule R M) (f : M →ₗ[R] M₂) : LinearMap.range (f.domRestrict K) = Submodule.map f K - LinearMap.submoduleImage.eq_1 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_10} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : ↥O →ₗ[R] M') (N : Submodule R M) : ϕ.submoduleImage N = Submodule.map ϕ (Submodule.comap O.subtype N) - Submodule.restrictScalars_map 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] [SMul R R₂] [Module R₂ M] [Module R M₂] [IsScalarTower R R₂ M] [IsScalarTower R R₂ M₂] (f : M →ₗ[R₂] M₂) (M' : Submodule R₂ M) : Submodule.restrictScalars R (Submodule.map f M') = Submodule.map (↑R f) (Submodule.restrictScalars R M') - Submodule.map_subtype_range_inclusion 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : p ≤ p') : Submodule.map p'.subtype (LinearMap.range (Submodule.inclusion h)) = p - Submodule.map_subtype_embedding_eq 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R ↥p) : (Submodule.MapSubtype.orderEmbedding p) p' = Submodule.map p.subtype p' - Submodule.coe_mapIic_apply 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) : ↑(p.mapIic q) = Submodule.map p.subtype q - LinearEquiv.ofSubmodules 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (q : Submodule R₂ M₂) (h : Submodule.map (↑e) p = q) : ↥p ≃ₛₗ[σ₁₂] ↥q - LinearEquiv.ofSubmodules_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : ↥p) : ↑((e.ofSubmodules p q h) x) = e ↑x - LinearEquiv.ofSubmodules_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : ↥q) : ↑((e.ofSubmodules p q h).symm x) = e.symm ↑x - Submodule.equivSubtypeMap 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) - Submodule.equivSubtypeMap_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R ↥p} (x : ↥q) : ↑((p.equivSubtypeMap q) x) = (p.subtype.domRestrict q) x - Submodule.equivSubtypeMap_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R ↥p} (x : ↥(Submodule.map p.subtype q)) : ↑↑((p.equivSubtypeMap q).symm x) = ↑x - LinearMap.map_span 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) : Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s) - Submodule.map_span 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) : Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s) - Submodule.span_image 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : F) : Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s) - LinearMap.map_injective 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.ker f = ⊥) : Function.Injective (Submodule.map f) - Submodule.span_image' 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) : Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s) - LinearMap.map_span_le 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N - Submodule.map_span_le 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) : Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N - Submodule.comap_map_eq 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (p : Submodule R M) : Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.ker f - Submodule.comap_map_eq_self 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} (h : LinearMap.ker f ≤ p) : Submodule.comap f (Submodule.map f p) = p - Submodule.comap_map_sup_of_comap_le 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} (le : Submodule.comap f q ≤ p) : Submodule.comap f (Submodule.map f p ⊔ q) = p - LinearMap.map_eq_top_iff 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.range f = ⊤) {p : Submodule R M} : Submodule.map f p = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤ - Submodule.map_iInf_of_ker_le 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective ⇑f) {ι : Sort u_9} {p : ι → Submodule R M} (h : LinearMap.ker f ≤ ⨅ i, p i) : Submodule.map f (⨅ i, p i) = ⨅ i, Submodule.map f (p i) - LinearMap.map_le_map_iff' 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : LinearMap.ker f = ⊥) {p p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' - Submodule.isCoatom_map_of_ker_le 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective ⇑f) {p : Submodule R M} (le : LinearMap.ker f ≤ p) (hp : IsCoatom p) : IsCoatom (Submodule.map f p) - LinearMap.map_le_map_iff 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) {p p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ LinearMap.ker f - Submodule.map_strict_mono_of_ker_inf_eq 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {p p' : Submodule R M} {f : F} (hab : p < p') (q : LinearMap.ker f ⊓ p = LinearMap.ker f ⊓ p') : Submodule.map f p < Submodule.map f p' - LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {p p' : Submodule R M} {f : F} (hab : p < p') (q : Submodule.map f p = Submodule.map f p') : LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' - Submodule.map_strict_mono_or_ker_sup_lt_ker_sup 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {p p' : Submodule R M} (f : F) (hab : p < p') : Submodule.map f p < Submodule.map f p' ∨ LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' - Submodule.map_lt_map_of_le_of_sup_lt_sup 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {p p' : Submodule R M} {f : F} (hab : p ≤ p') (h : p ⊔ LinearMap.ker f < p' ⊔ LinearMap.ker f) : Submodule.map f p < Submodule.map f p' - Submodule.map_subtype_span_singleton 📋 Mathlib.LinearAlgebra.Span.Basic
{R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (x : ↥p) : Submodule.map p.subtype (Submodule.span R {x}) = Submodule.span R {↑x} - Submodule.map₂_map_right 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {N₂ : Type u_6} [AddCommMonoid N₂] [Module R N₂] (f : M →ₗ[R] N₂ →ₗ[R] P) (g : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) : Submodule.map₂ f p (Submodule.map g q) = Submodule.map₂ (f.compl₂ g) p q - Submodule.map_map₂ 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {P₂ : Type u_7} [AddCommMonoid P₂] [Module R P₂] (f : P →ₗ[R] P₂) (g : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : Submodule.map f (Submodule.map₂ g p q) = Submodule.map₂ (g.compr₂ f) p q - Submodule.map₂_map_left 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {M₂ : Type u_5} [AddCommMonoid M₂] [Module R M₂] (f : M₂ →ₗ[R] N →ₗ[R] P) (g : M →ₗ[R] M₂) (p : Submodule R M) (q : Submodule R N) : Submodule.map₂ f (Submodule.map g p) q = Submodule.map₂ (f ∘ₗ g) p q - Submodule.map₂_map_map 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {M₂ : Type u_5} {N₂ : Type u_6} [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M₂] [Module R N₂] (f : M₂ →ₗ[R] N₂ →ₗ[R] P) (g : M →ₗ[R] M₂) (h : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) : Submodule.map₂ f (Submodule.map g p) (Submodule.map h q) = Submodule.map₂ (f.compl₁₂ g h) p q - Submodule.map₂_span_singleton_eq_map 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) : Submodule.map₂ f (Submodule.span R {m}) = Submodule.map (f m) - Submodule.map₂_span_singleton_eq_map_flip 📋 Mathlib.Algebra.Module.Submodule.Bilinear
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) : Submodule.map₂ f s (Submodule.span R {n}) = Submodule.map (f.flip n) s - NonUnitalSubalgebra.map_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
{F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule - Finsupp.lmapDomain_supported 📋 Mathlib.LinearAlgebra.Finsupp.Supported
{α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (s : Set α) : Submodule.map (Finsupp.lmapDomain M R f) (Finsupp.supported M R s) = Finsupp.supported M R (f '' s) - Submodule.set_smul_eq_map 📋 Mathlib.Algebra.Module.Submodule.Pointwise
{R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (sR : Set R) (N : Submodule R M) [SMulCommClass R R ↥N] : sR • N = Submodule.map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) - Submodule.map_one 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : Submodule.map f.toLinearMap 1 = 1 - Submodule.map_op_one 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.map (↑(MulOpposite.opLinearEquiv R)) 1 = 1 - Submodule.mapHom_apply 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (p : Submodule R A) : (Submodule.mapHom f) p = Submodule.map f.toLinearMap p - Submodule.map_unop_one 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) 1 = 1 - Submodule.map_pow 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) : Submodule.map f.toLinearMap (M ^ n) = Submodule.map f.toLinearMap M ^ n - Submodule.map_mul 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N - Submodule.map_div 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (I J : Submodule R A) (h : A ≃ₐ[R] B) : Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J - Submodule.singleton_smul 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [Algebra R A] (a : A) (M : Submodule R A) : Set.up {a} • M = Submodule.map (LinearMap.mulLeft R a) M - Submodule.map_op_pow 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) (n : ℕ) : Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) M ^ n - Submodule.map_unop_pow 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (n : ℕ) (M : Submodule R Aᵐᵒᵖ) : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M ^ n - Submodule.map_op_mul 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R A) : Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) N * Submodule.map (↑(MulOpposite.opLinearEquiv R)) M - Submodule.map_unop_mul 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M N : Submodule R Aᵐᵒᵖ) : Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M * N) = Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M - Submodule.span_algebraMap_image 📋 Mathlib.Algebra.Algebra.Tower
{R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (a : Set R) : Submodule.span R (⇑(algebraMap R S) '' a) = Submodule.map (Algebra.linearMap R S) (Submodule.span R a) - Submodule.span_algebraMap_image_of_tower 📋 Mathlib.Algebra.Algebra.Tower
{R : Type u} [CommSemiring R] {S : Type u_1} {T : Type u_2} [CommSemiring S] [Semiring T] [Module R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) : Submodule.span R (⇑(algebraMap S T) '' a) = Submodule.map (↑R (Algebra.linearMap S T)) (Submodule.span R a) - Subalgebra.map_toSubmodule 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
{R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} : Subalgebra.toSubmodule (Subalgebra.map f S) = Submodule.map f.toLinearMap (Subalgebra.toSubmodule S) - Finsupp.span_image_eq_map_linearCombination 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
{α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : Submodule.span R (v '' s) = Submodule.map (Finsupp.linearCombination R v) (Finsupp.supported R R s) - Submodule.map_le_smul_top 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (f : R →ₗ[R] M) : Submodule.map f I ≤ I • ⊤ - Submodule.map_smul'' 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (I : Ideal R) (N : Submodule R M) {M' : Type w} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') : Submodule.map f (I • N) = I • Submodule.map f N - Submodule.map_pointwise_smul 📋 Mathlib.RingTheory.Ideal.Operations
{R : Type u} {M : Type v} {M' : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (r : R) (N : Submodule R M) (f : M →ₗ[R] M') : Submodule.map f (r • N) = r • Submodule.map f N - Ideal.map_eq_submodule_map 📋 Mathlib.RingTheory.Ideal.Maps
{R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : RingHomSurjective f] (I : Ideal R) : Ideal.map f I = Submodule.map f.toSemilinearMap I - Submodule.fst_map_fst 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : Submodule.map (LinearMap.fst R M M₂) (Submodule.fst R M M₂) = ⊤ - Submodule.fst_map_snd 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : Submodule.map (LinearMap.snd R M M₂) (Submodule.fst R M M₂) = ⊥ - Submodule.snd_map_fst 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : Submodule.map (LinearMap.fst R M M₂) (Submodule.snd R M M₂) = ⊥ - Submodule.snd_map_snd 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : Submodule.map (LinearMap.snd R M M₂) (Submodule.snd R M M₂) = ⊤ - Submodule.prod_map_fst 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) : Submodule.map (LinearMap.fst R M M₂) (p.prod q) = p - Submodule.prod_map_snd 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) : Submodule.map (LinearMap.snd R M M₂) (p.prod q) = q - Submodule.map_inl 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) : Submodule.map (LinearMap.inl R M M₂) p = p.prod ⊥ - Submodule.map_inr 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (q : Submodule R M₂) : Submodule.map (LinearMap.inr R M M₂) q = ⊥.prod q - LinearMap.coprod_map_prod 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M) (S' : Submodule R M₂) : Submodule.map (f.coprod g) (S.prod S') = Submodule.map f S ⊔ Submodule.map g S' - LinearMap.map_coprod_prod 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M) (q : Submodule R M₂) : Submodule.map (f.coprod g) (p.prod q) = Submodule.map f p ⊔ Submodule.map g q - LinearMap.prod_eq_sup_map 📋 Mathlib.LinearAlgebra.Prod
{R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) : p.prod q = Submodule.map (LinearMap.inl R M M₂) p ⊔ Submodule.map (LinearMap.inr R M M₂) q - Submodule.le_prod_iff 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} : q ≤ p₁.prod p₂ ↔ Submodule.map (LinearMap.fst R M M₂) q ≤ p₁ ∧ Submodule.map (LinearMap.snd R M M₂) q ≤ p₂ - Submodule.prod_le_iff 📋 Mathlib.LinearAlgebra.Prod
(R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} : p₁.prod p₂ ≤ q ↔ Submodule.map (LinearMap.inl R M M₂) p₁ ≤ q ∧ Submodule.map (LinearMap.inr R M M₂) p₂ ≤ q - Submodule.iSup_map_single 📋 Mathlib.LinearAlgebra.Pi
{R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} [DecidableEq ι] [Finite ι] : ⨆ i, Submodule.map (LinearMap.single R φ i) (p i) = Submodule.pi Set.univ p - Submodule.iSup_map_single_le 📋 Mathlib.LinearAlgebra.Pi
{R : Type u} {ι : Type x} [Semiring R] {φ : ι → Type u_1} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} [DecidableEq ι] : ⨆ i, Submodule.map (LinearMap.single R φ i) (p i) ≤ Submodule.pi I p - Submodule.baseChange_eq_span 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
{R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.baseChange A p = Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) p) - Submodule.map_range_rTensor_subtype_lid 📋 Mathlib.RingTheory.TensorProduct.Basic
{R : Type u_1} {Q : Type u_2} [CommSemiring R] [AddCommMonoid Q] [Module R Q] {I : Submodule R R} : Submodule.map (TensorProduct.lid R Q) (LinearMap.range (LinearMap.rTensor Q I.subtype)) = I • ⊤ - rank_map_le 📋 Mathlib.LinearAlgebra.Dimension.Basic
{R : Type u} {M M₁ : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) : Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p - lift_rank_map_le 📋 Mathlib.LinearAlgebra.Dimension.Basic
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) : Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ Cardinal.lift.{v', v} (Module.rank R ↥p) - LinearEquiv.rank_map_eq 📋 Mathlib.LinearAlgebra.Dimension.Basic
{R : Type u} {M M₁ : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] (f : M ≃ₗ[R] M₁) (p : Submodule R M) : Module.rank R ↥(Submodule.map (↑f) p) = Module.rank R ↥p - LinearEquiv.lift_rank_map_eq 📋 Mathlib.LinearAlgebra.Dimension.Basic
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (f : M ≃ₗ[R] M') (p : Submodule R M) : Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map (↑f) p)) = Cardinal.lift.{v', v} (Module.rank R ↥p) - LinearEquiv.finrank_map_eq 📋 Mathlib.LinearAlgebra.Dimension.Finrank
{R : Type u} {M : Type v} {N : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) (p : Submodule R M) : Module.finrank R ↥(Submodule.map (↑f) p) = Module.finrank R ↥p - Submodule.finrank_map_subtype_eq 📋 Mathlib.LinearAlgebra.Dimension.Finrank
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) : Module.finrank R ↥(Submodule.map p.subtype q) = Module.finrank R ↥q - LinearMap.iterateMapComap.eq_1 📋 Mathlib.Algebra.Module.Submodule.IterateMapComap
{R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (n : ℕ) : f.iterateMapComap i n = (fun K => Submodule.comap f (Submodule.map i K))^[n] - LinearMap.iterateMapComap_le_succ 📋 Mathlib.Algebra.Module.Submodule.IterateMapComap
{R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (h : Submodule.map f K ≤ Submodule.map i K) (n : ℕ) : f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K - Submodule.mkQ_map_self 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule.map p.mkQ p = ⊥ - Submodule.Quotient.equiv 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : Submodule.map f P = Q) : (M ⧸ P) ≃ₗ[R] N ⧸ Q - Submodule.map_mkQ_eq_top 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : Submodule.map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤ - Submodule.comap_map_mkQ 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : Submodule.comap p.mkQ (Submodule.map p.mkQ p') = p ⊔ p' - Submodule.Quotient.equiv_refl 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hf : Submodule.map (↑(LinearEquiv.refl R M)) P = Q) : Submodule.Quotient.equiv P Q (LinearEquiv.refl R M) hf = P.quotEquivOfEq Q ⋯ - Submodule.ker_liftQ 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : LinearMap.ker (p.liftQ f h) = Submodule.map p.mkQ (LinearMap.ker f) - Submodule.comap_liftQ 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : Submodule.comap (p.liftQ f h) q = Submodule.map p.mkQ (Submodule.comap f q) - Submodule.map_liftQ 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) (q : Submodule R (M ⧸ p)) : Submodule.map (p.liftQ f h) q = Submodule.map f (Submodule.comap p.mkQ q) - Submodule.Quotient.equiv.congr_simp 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f f✝ : M ≃ₗ[R] N) (e_f : f = f✝) (hf : Submodule.map f P = Q) : Submodule.Quotient.equiv P Q f hf = Submodule.Quotient.equiv P Q f✝ ⋯ - Submodule.Quotient.equiv_apply 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : Submodule.map f P = Q) (a : M ⧸ P) : (Submodule.Quotient.equiv P Q f hf) a = (P.mapQ Q ↑f ⋯) a - Submodule.Quotient.equiv_symm_apply 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : Submodule.map f P = Q) (a : N ⧸ Q) : (Submodule.Quotient.equiv P Q f hf).symm a = (Q.mapQ P ↑f.symm ⋯) a - Submodule.strictMono_comap_prod_map 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : StrictMono fun m => (Submodule.comap p.subtype m, Submodule.map p.mkQ m) - Submodule.Quotient.equiv_symm 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_5} {M : Type u_6} {N : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : Submodule.map f P = Q) : (Submodule.Quotient.equiv P Q f hf).symm = Submodule.Quotient.equiv Q P f.symm ⋯ - Submodule.Quotient.equiv_trans 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} {O : Type u_6} [AddCommGroup N] [Module R N] [AddCommGroup O] [Module R O] (P : Submodule R M) (Q : Submodule R N) (S : Submodule R O) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O) (he : Submodule.map e P = Q) (hf : Submodule.map f Q = S) (hef : Submodule.map (e ≪≫ₗ f) P = S) : Submodule.Quotient.equiv P S (e ≪≫ₗ f) hef = Submodule.Quotient.equiv P Q e he ≪≫ₗ Submodule.Quotient.equiv Q S f hf - Submodule.FG.map 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} {P : Type u_4} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (f : M →ₛₗ[σ] P) {N : Submodule R M} (hs : N.FG) : (Submodule.map f N).FG - Submodule.fg_of_fg_map_injective 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} {P : Type u_4} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (f : M →ₛₗ[σ] P) (hf : Function.Injective ⇑f) {N : Submodule R M} (hfn : (Submodule.map f N).FG) : N.FG - Submodule.fg_of_fg_map 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_4} {M : Type u_5} {P : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) {N : Submodule R M} (hfn : (Submodule.map f N).FG) : N.FG - Module.Finite.map 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (p : Submodule R M) [Module.Finite R ↥p] (f : M →ₗ[R] N) : Module.Finite R ↥(Submodule.map f p) - Submodule.card_quotient_mul_card_quotient 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (hST : T ≤ S) : Nat.card ↥(Submodule.map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T) - Submodule.quotientQuotientEquivQuotientAux 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S ≤ T) : (M ⧸ S) ⧸ Submodule.map S.mkQ T →ₗ[R] M ⧸ T - Submodule.quotientQuotientEquivQuotient 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S ≤ T) : ((M ⧸ S) ⧸ Submodule.map S.mkQ T) ≃ₗ[R] M ⧸ T - Submodule.quotientQuotientEquivQuotientAux.congr_simp 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S ≤ T) : S.quotientQuotientEquivQuotientAux T h = S.quotientQuotientEquivQuotientAux T h - Submodule.quotientQuotientEquivQuotientSup 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) : ((M ⧸ S) ⧸ Submodule.map S.mkQ T) ≃ₗ[R] M ⧸ S ⊔ T - Submodule.quotientQuotientEquivQuotientAux_mk_mk 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S ≤ T) (x : M) : (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk (Submodule.Quotient.mk x)) = Submodule.Quotient.mk x - Submodule.quotientQuotientEquivQuotientAux_mk 📋 Mathlib.LinearAlgebra.Isomorphisms
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S ≤ T) (x : M ⧸ S) : (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk x) = (S.mapQ T LinearMap.id h) x - Submodule.fg_of_fg_map_of_fg_inf_ker 📋 Mathlib.RingTheory.Finiteness.Finsupp
{R : Type u_1} {M : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] (f : M →ₗ[R] P) {s : Submodule R M} (hs1 : (Submodule.map f s).FG) (hs2 : (s ⊓ LinearMap.ker f).FG) : s.FG - Submodule.IsPrincipal.map 📋 Mathlib.RingTheory.PrincipalIdealDomain
{R : Type u} {M : Type v} {N : Type u_2} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) {S : Submodule R M} (hI : S.IsPrincipal) : (Submodule.map f S).IsPrincipal
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle
command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→
and∀
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision ee8c038
serving mathlib revision 7a9e177