Theorems · Definition · group theory

Function.Surjective.rootableBy

{A : Type u_1} →
  {B : Type u_2} →
    {α : Type u_3} →
      [inst : Zero α] →
        [inst_1 : Monoid A] →
          [inst_2 : Monoid B] →
            [inst_3 : Pow A α] →
              [inst_4 : Pow B α] →
                [RootableBy A α] →
                  (f : A → B) → Function.Surjective f → (∀ (a : A) (n : α), f (a ^ n) = f a ^ n) → RootableBy B α

If f : A → B is a surjective homomorphism and A is α-rootable, then B is also α-rootable.

Defined in: Mathlib.GroupTheory.Divisible
Cited by: 0 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero Monoid Monoid Pow Pow RootableBy

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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
rootableByOfPowLeftSurjproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.