Theorems · Definition · group theory

Function.Injective.commGroupWithZero

{G₀ : Type u_2} →
  {G₀' : Type u_4} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    (f : G₀' → G₀) →
                      Function.Injective f →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : G₀'), f (x * y) = f x * f y) →
                              (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) →
                                (∀ (x y : G₀'), f (x / y) = f x / f y) →
                                  (∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) →
                                    (∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) → CommGroupWithZero G₀'

Pull back a CommGroupWithZero along an injective function. See note [reducible non-instances].

Defined in

Mathlib.Algebra.GroupWithZero.InjSurj

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

CommGroupWithZeroZeroMulOneInvDivPowPow