Theorems · Definition · group theory

RootableBy.recOn

{A : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid A] →
      [inst_1 : Pow A α] →
        [inst_2 : Zero α] →
          {motive : RootableBy A α → Sort u} →
            (t : RootableBy A α) →
              ((root : A → α → A) →
                  (root_zero : ∀ (a : A), root a 0 = 1) →
                    (root_cancel : ∀ {n : α} (a : A), n ≠ 0 → root a n ^ n = a) →
                      motive { root := root, root_zero := root_zero, root_cancel := root_cancel }) →
                motive t

Defined in: Mathlib.GroupTheory.Divisible
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms
Assumes: Monoid Pow Zero

Mathlib docs Source Loogle LeanSearch

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.