Mathlib Map

Theorems · Definition · group theory

RootableBy.root

{A : Type u_1} →
  {α : Type u_2} → {inst : Monoid A} → {inst_1 : Pow A α} → {inst_2 : Zero α} → [self : RootableBy A α] → A → α → A

The root function

Defined in
Mathlib.GroupTheory.Divisible
Cited by
3 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
RootableBy
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

RootableBy.surjective_pow · cited by 2RootableBy.surjective_powRootableBy.root_cancel · cited by 1RootableBy.root_cancelRootableBy.root_zero · cited by 0RootableBy.root_zeroGroup.rootableByIntOfRootableByNat · cited by 0Group.rootableByIntOfRoot…Group.rootableByNatOfRootableByInt · cited by 0Group.rootableByNatOfRoot…Monoid · cited by 3887MonoidRootableBy · cited by 6RootableByRootableBy.rootCITED BYCITES

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 by5

Results whose statement or proof uses this declaration.