Theorems · Theorem · ring theory

iSupIndep.linearEquiv.congr_simp

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤),
  ind.linearEquiv iSup_top = ind.linearEquiv iSup_top

Defined in: Mathlib.RingTheory.SimpleModule.Isotypic
Cited by: 0 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Ring AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
Top.topstatement and proof · cited by 9,680
Ringstatement and proof · cited by 7,463
Submodulestatement and proof · cited by 7,192
LinearEquivstatement · cited by 3,317
iSupstatement and proof · cited by 2,415
DFinsuppstatement · cited by 694
iSupIndepstatement and proof · cited by 100
iSupIndep.linearEquivstatement and proof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.