Theorems · Theorem · ring theory

DirectSum.isInternal_biSup_submodule_of_iSupIndep

∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (s : Set ι),
  (iSupIndep fun i => A ↑i) → DirectSum.IsInternal fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Defined in: Mathlib.Algebra.DirectSum.Module
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring DecidableEq AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites27

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

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
Top.topproof · cited by 9,680
Ringstatement and proof · cited by 7,463
Submodulestatement and proof · cited by 7,192
Set.Elemstatement and proof · cited by 7,166
iSupstatement and proof · cited by 2,415
Set.Iicproof · cited by 1,111
OrderIsoproof · cited by 874

Cited by1

Results whose statement or proof uses this declaration.

LinearMap.trace_eq_sum_trace_restrict_of_eq_biSupproof · cited by 1