Theorems · Theorem · nonassociative algebras

RootPairing.IsRootSystem.span_coroot_eq_top

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsRootSystem], Submodule.span R (Set.range ⇑P.coroot) = ⊤

Defined in: Mathlib.LinearAlgebra.RootSystem.Defs
Cited by: 4 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Quot.sound
Assumes: RootPairing.IsRootSystem

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

DFunLike.coestatement · cited by 62,936
Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Top.topstatement · cited by 9,680
Submodulestatement · cited by 7,192
Set.rangestatement · cited by 4,705
Submodule.spanstatement · cited by 1,504
Function.Embeddingstatement · cited by 988
RootPairingstatement and proof · cited by 710
RootPairing.corootstatement · cited by 123
RootPairing.IsRootSystemstatement and proof · cited by 50

Cited by4

Results whose statement or proof uses this declaration.

RootPairing.finrank_rootSpanInproof · cited by 3
LieAlgebra.IsKilling.biSup_corootSpace_eq_topproof · cited by 2
RootPairing.eq_zero_iff_forall_coroot'_eq_zeroproof · cited by 2
RootPairing.eq_top_of_mem_invtSubmodule_of_forall_eq_univproof · cited by 0