Mathlib Map

Theorems · Definition · group theory

RootableBy.ctorIdx

{A : Type u_1} → {α : Type u_2} → {inst : Monoid A} → {inst_1 : Pow A α} → {inst_2 : Zero α} → RootableBy A α → ℕ
Defined in
Mathlib.GroupTheory.Divisible
Cited by
0 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms

Around this declaration

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

Cites2

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

  • Monoidstatement and proof · cited by 3,887
  • RootableBystatement and proof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.