Theorems · Theorem · linear algebra

LinearMap.mapsTo_biSup_of_mapsTo

∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  {N : ι → Submodule R M} (s : Set ι) {f : Module.End R M},
  (∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) → Set.MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Defined in: Mathlib.Algebra.DirectSum.LinearMap
Cited by: 2 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
SetLike.coestatement and proof · cited by 8,199
Submodulestatement and proof · cited by 7,192
iSupstatement and proof · cited by 2,415
Module.Endstatement and proof · cited by 774
Set.MapsTostatement and proof · cited by 732
Submodule.mapproof · cited by 614

Cited by2

Results whose statement or proof uses this declaration.

LieModule.exists_forall_mem_corootSpace_smul_add_eq_zeroproof · cited by 1
LinearMap.trace_eq_sum_trace_restrict_of_eq_biSupstatement · cited by 1