Loogle!

Result

Found 341 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₂] {ι : Type 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_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_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_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} : Submodule.map (↑e) p = Submodule.comap (↑e.symm) p
• 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_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_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_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_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₂_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_1 📋 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_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.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} [Ring R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) {S : Submodule R M} (hI : S.IsPrincipal) : (Submodule.map f S).IsPrincipal
• Submodule.IsPrincipal.generator_map_dvd_of_mem 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} {M : Type v} [AddCommMonoid M] [CommRing R] [Module R M] {N : Submodule R M} (ϕ : M →ₗ[R] R) [(Submodule.map ϕ N).IsPrincipal] {x : M} (hx : x ∈ N) : Submodule.IsPrincipal.generator (Submodule.map ϕ N) ∣ ϕ x
• Submodule.finrank_map_le 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [StrongRankCondition R] [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R ↥p] : Module.finrank R ↥(Submodule.map f p) ≤ Module.finrank R ↥p
• LinearPMap.graph_map_fst_eq_domain 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : Submodule.map (LinearMap.fst R E F) f.graph = f.domain
• Submodule.toLinearPMap_domain 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) : g.toLinearPMap.domain = Submodule.map (LinearMap.fst R E F) g
• LinearPMap.inverse.eq_1 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : f.inverse = (Submodule.map (LinearEquiv.prodComm R E F) f.graph).toLinearPMap
• Submodule.valFromGraph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) : F
• LinearPMap.neg_graph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : (-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
• Submodule.existsUnique_from_graph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) : ∃! b, (a, b) ∈ g
• Submodule.valFromGraph_mem 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) {a : E} (ha : a ∈ Submodule.map (LinearMap.fst R E F) g) : (a, Submodule.valFromGraph hg ha) ∈ g
• LinearPMap.smul_graph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] (f : E →ₗ.[R] F) (z : M) : (z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
• LinearPMap.graph_map_snd_eq_range 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : Submodule.map (LinearMap.snd R E F) f.graph = LinearMap.range f.toFun
• Submodule.mem_graph_toLinearPMap 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (x : ↥(Submodule.map (LinearMap.fst R E F) g)) : (↑x, ↑g.toLinearPMap x) ∈ g
• Submodule.toLinearPMapAux 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) : ↥(Submodule.map (LinearMap.fst R E F) g) →ₗ[R] F
• Submodule.toLinearPMap_apply_aux 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {g : Submodule R (E × F)} (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) (x : ↥(Submodule.map (LinearMap.fst R E F) g)) : ↑g.toLinearPMap x = Submodule.valFromGraph hg ⋯
• Submodule.toLinearPMap_range 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (g : Submodule R (E × F)) (hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0) : LinearMap.range g.toLinearPMap.toFun = Submodule.map (LinearMap.snd R E F) g
• LinearPMap.graph.eq_1 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (f : E →ₗ.[R] F) : f.graph = Submodule.map (f.domain.subtype.prodMap LinearMap.id) f.toFun.graph
• LinearPMap.inverse_graph 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) : f.inverse.graph = Submodule.map (LinearEquiv.prodComm R E F) f.graph
• LinearPMap.mem_inverse_graph_snd_eq_zero 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] {f : E →ₗ.[R] F} (hf : LinearMap.ker f.toFun = ⊥) (x : F × E) (hv : x ∈ Submodule.map (LinearEquiv.prodComm R E F) f.graph) (hv' : x.1 = 0) : x.2 = 0

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 find tsum_lt_tsum even though the hypothesis f 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 19971e9 serving mathlib revision bce1d65