Lifting algebraic data classes along injective/surjective maps

This file provides definitions that are meant to deal with situations such as the following:

Suppose that G is a group, and H is a type endowed with One H, Mul H, and Inv H. Suppose furthermore, that f : G → H is a surjective map that respects the multiplication, and the unit elements. Then H satisfies the group axioms.

The relevant definition in this case is Function.Surjective.group. Dually, there is also Function.Injective.group. And there are versions for (additive) (commutative) semigroups/monoids.

Note that the nsmul and zsmul hypotheses in the declarations in this file are declared as ∀ x n, f (n • x) = n • f x, with the binders in a slightly unnatural order, as they are to_additiveized from the versions for ^.

Injective

@[reducible, inline]

abbrev Function.Injective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [Semigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : Semigroup M₁

A type endowed with * is a semigroup, if it admits an injective map that preserves * to a semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddSemigroup M₁

A type endowed with + is an additive semigroup, if it admits an injective map that preserves + to an additive semigroup.

@[reducible, inline]

abbrev Function.Injective.commMagma {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommMagma M₁

A type endowed with * is a commutative magma, if it admits a surjective map that preserves * from a commutative magma.

@[reducible, inline]

abbrev Function.Injective.addCommMagma {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommMagma M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommMagma M₁

A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

@[reducible, inline]

abbrev Function.Injective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [CommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommSemigroup M₁

A type endowed with * is a commutative semigroup, if it admits an injective map that preserves * to a commutative semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommSemigroup M₁

A type endowed with + is an additive commutative semigroup,if it admits an injective map that preserves + to an additive commutative semigroup.

theorem Function.Injective.isLeftCancelMul {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [Mul M₂] [IsLeftCancelMul M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : IsLeftCancelMul M₁

A type has left-cancellative multiplication, if it admits an injective map that preserves * to another type with left-cancellative multiplication.

theorem Function.Injective.isLeftCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsLeftCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : IsLeftCancelAdd M₁

A type has left-cancellative addition, if it admits an injective map that preserves + to another type with left-cancellative addition.

theorem Function.Injective.isRightCancelMul {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [Mul M₂] [IsRightCancelMul M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : IsRightCancelMul M₁

A type has right-cancellative multiplication, if it admits an injective map that preserves * to another type with right-cancellative multiplication.

theorem Function.Injective.isRightCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsRightCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : IsRightCancelAdd M₁

A type has right-cancellative addition, if it admits an injective map that preserves + to another type with right-cancellative addition.

theorem Function.Injective.isCancelMul {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [Mul M₂] [IsCancelMul M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : IsCancelMul M₁

A type has cancellative multiplication, if it admits an injective map that preserves * to another type with cancellative multiplication.

theorem Function.Injective.isCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : IsCancelAdd M₁

A type has cancellative addition, if it admits an injective map that preserves + to another type with cancellative addition.

@[reducible, inline]

abbrev Function.Injective.leftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : LeftCancelSemigroup M₁

A type endowed with * is a left cancel semigroup, if it admits an injective map that preserves * to a left cancel semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addLeftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddLeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddLeftCancelSemigroup M₁

A type endowed with + is an additive left cancel semigroup, if it admits an injective map that preserves + to an additive left cancel semigroup.

@[reducible, inline]

abbrev Function.Injective.rightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : RightCancelSemigroup M₁

A type endowed with * is a right cancel semigroup, if it admits an injective map that preserves * to a right cancel semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addRightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddRightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddRightCancelSemigroup M₁

A type endowed with + is an additive right cancel semigroup, if it admits an injective map that preserves + to an additive right cancel semigroup.

@[reducible, inline]

abbrev Function.Injective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [MulOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : MulOneClass M₁

A type endowed with 1 and * is a MulOneClass, if it admits an injective map that preserves 1 and * to a MulOneClass. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [AddZeroClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddZeroClass M₁

A type endowed with 0 and + is an AddZeroClass, if it admits an injective map that preserves 0 and + to an AddZeroClass.

@[reducible, inline]

abbrev Function.Injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Monoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁

A type endowed with 1 and * is a monoid, if it admits an injective map that preserves 1 and * to a monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddMonoid M₁

A type endowed with 0 and + is an additive monoid, if it admits an injective map that preserves 0 and + to an additive monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.leftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁

A type endowed with 1 and * is a left cancel monoid, if it admits an injective map that preserves 1 and * to a left cancel monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addLeftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddLeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddLeftCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid, if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

@[reducible, inline]

abbrev Function.Injective.rightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁

A type endowed with 1 and * is a right cancel monoid, if it admits an injective map that preserves 1 and * to a right cancel monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addRightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddRightCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddRightCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

@[reducible, inline]

abbrev Function.Injective.cancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [CancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoid M₁

A type endowed with 1 and * is a cancel monoid, if it admits an injective map that preserves 1 and * to a cancel monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddCancelMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

@[reducible, inline]

abbrev Function.Injective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [CommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₁

A type endowed with 1 and * is a commutative monoid, if it admits an injective map that preserves 1 and * to a commutative monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCommMonoid M₁

A type endowed with 0 and + is an additive commutative monoid, if it admits an injective map that preserves 0 and + to an additive commutative monoid.

@[reducible, inline]

abbrev Function.Injective.cancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [CancelCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁

A type endowed with 1 and * is a cancel commutative monoid if it admits an injective map that preserves 1 and * to a cancel commutative monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addCancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCancelCommMonoid M₁

A type endowed with 0 and + is an additive cancel commutative monoid if it admits an injective map that preserves 0 and + to an additive cancel commutative monoid.

@[reducible, inline]

abbrev Function.Injective.involutiveInv {M₂ : Type u_2} {M₁ : Type u_3} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁

A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

@[reducible, inline]

abbrev Function.Injective.involutiveNeg {M₂ : Type u_2} {M₁ : Type u_3} [Neg M₁] [InvolutiveNeg M₂] (f : M₁ → M₂) (hf : Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) : InvolutiveNeg M₁

A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

@[reducible, inline]

abbrev Function.Injective.invOneClass {M₁ : Type u_1} {M₂ : Type u_2} [One M₁] [Inv M₁] [InvOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvOneClass M₁

A type endowed with 1 and ⁻¹ is a InvOneClass, if it admits an injective map that preserves 1 and ⁻¹ to a InvOneClass. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.negZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [Neg M₁] [NegZeroClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (inv : ∀ (x : M₁), f (-x) = -f x) : NegZeroClass M₁

A type endowed with 0 and unary - is an NegZeroClass, if it admits an injective map that preserves 0 and unary - to an NegZeroClass.

@[reducible, inline]

abbrev Function.Injective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [DivInvMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₁

A type endowed with 1, *, ⁻¹, and / is a DivInvMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [SubNegMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubNegMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubNegMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

@[reducible, inline]

abbrev Function.Injective.divInvOneMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [DivInvOneMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvOneMonoid M₁

A type endowed with 1, *, ⁻¹, and / is a DivInvOneMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivInvOneMonoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.subNegZeroMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [SubNegZeroMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubNegZeroMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubNegZeroMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubNegZeroMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

@[reducible, inline]

abbrev Function.Injective.divisionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [DivisionMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionMonoid M₁

A type endowed with 1, *, ⁻¹, and / is a DivisionMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivisionMonoid. See note [reducible non-instances]

@[reducible, inline]

abbrev Function.Injective.subtractionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [SubtractionMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubtractionMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubtractionMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

@[reducible, inline]

abbrev Function.Injective.divisionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [DivisionCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁

A type endowed with 1, *, ⁻¹, and / is a DivisionCommMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivisionCommMonoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.subtractionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [SubtractionCommMonoid M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubtractionCommMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubtractionCommMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionCommMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

@[reducible, inline]

abbrev Function.Injective.group {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [Group M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₁

A type endowed with 1, * and ⁻¹ is a group, if it admits an injective map that preserves 1, * and ⁻¹ to a group. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [AddGroup M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddGroup M₁

A type endowed with 0 and + is an additive group, if it admits an injective map that preserves 0 and + to an additive group.

@[reducible, inline]

abbrev Function.Injective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ℕ] [Inv M₁] [Div M₁] [Pow M₁ ℤ] [CommGroup M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁

A type endowed with 1, * and ⁻¹ is a commutative group, if it admits an injective map that preserves 1, * and ⁻¹ to a commutative group. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul ℕ M₁] [Neg M₁] [Sub M₁] [SMul ℤ M₁] [AddCommGroup M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddCommGroup M₁

A type endowed with 0 and + is an additive commutative group, if it admits an injective map that preserves 0 and + to an additive commutative group.

Surjective

@[reducible, inline]

abbrev Function.Surjective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [Semigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : Semigroup M₂

A type endowed with * is a semigroup, if it admits a surjective map that preserves * from a semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddSemigroup M₂

A type endowed with + is an additive semigroup, if it admits a surjective map that preserves + from an additive semigroup.

@[reducible, inline]

abbrev Function.Surjective.commMagma {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [CommMagma M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommMagma M₂

A type endowed with * is a commutative semigroup, if it admits a surjective map that preserves * from a commutative semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addCommMagma {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddCommMagma M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommMagma M₂

A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

@[reducible, inline]

abbrev Function.Surjective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [CommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommSemigroup M₂

A type endowed with * is a commutative semigroup, if it admits a surjective map that preserves * from a commutative semigroup. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddCommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommSemigroup M₂

A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

@[reducible, inline]

abbrev Function.Surjective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [MulOneClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : MulOneClass M₂

A type endowed with 1 and * is a MulOneClass, if it admits a surjective map that preserves 1 and * from a MulOneClass. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [AddZeroClass M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddZeroClass M₂

A type endowed with 0 and + is an AddZeroClass, if it admits a surjective map that preserves 0 and + to an AddZeroClass.

@[reducible, inline]

abbrev Function.Surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ℕ] [Monoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₂

A type endowed with 1 and * is a monoid, if it admits a surjective map that preserves 1 and * to a monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul ℕ M₂] [AddMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddMonoid M₂

A type endowed with 0 and + is an additive monoid, if it admits a surjective map that preserves 0 and + to an additive monoid. This version takes a custom nsmul as a [SMul ℕ M₂] argument.

@[reducible, inline]

abbrev Function.Surjective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ℕ] [CommMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₂

A type endowed with 1 and * is a commutative monoid, if it admits a surjective map that preserves 1 and * from a commutative monoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul ℕ M₂] [AddCommMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCommMonoid M₂

A type endowed with 0 and + is an additive commutative monoid, if it admits a surjective map that preserves 0 and + to an additive commutative monoid.

@[reducible, inline]

abbrev Function.Surjective.involutiveInv {M₁ : Type u_1} {M₂ : Type u_3} [Inv M₂] [InvolutiveInv M₁] (f : M₁ → M₂) (hf : Surjective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₂

A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

@[reducible, inline]

abbrev Function.Surjective.involutiveNeg {M₁ : Type u_1} {M₂ : Type u_3} [Neg M₂] [InvolutiveNeg M₁] (f : M₁ → M₂) (hf : Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) : InvolutiveNeg M₂

A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

@[reducible, inline]

abbrev Function.Surjective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ℕ] [Inv M₂] [Div M₂] [Pow M₂ ℤ] [DivInvMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₂

A type endowed with 1, *, ⁻¹, and / is a DivInvMonoid if it admits a surjective map that preserves 1, *, ⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul ℕ M₂] [Neg M₂] [Sub M₂] [SMul ℤ M₂] [SubNegMonoid M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubNegMonoid M₂

A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits a surjective map that preserves 0, +, unary -, and binary - to a SubNegMonoid.

@[reducible, inline]

abbrev Function.Surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ℕ] [Inv M₂] [Div M₂] [Pow M₂ ℤ] [Group M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₂

A type endowed with 1, * and ⁻¹ is a group, if it admits a surjective map that preserves 1, * and ⁻¹ to a group. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul ℕ M₂] [Neg M₂] [Sub M₂] [SMul ℤ M₂] [AddGroup M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddGroup M₂

A type endowed with 0 and + is an additive group, if it admits a surjective map that preserves 0 and + to an additive group.

@[reducible, inline]

abbrev Function.Surjective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ℕ] [Inv M₂] [Div M₂] [Pow M₂ ℤ] [CommGroup M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂

A type endowed with 1, *, ⁻¹, and / is a commutative group, if it admits a surjective map that preserves 1, *, ⁻¹, and / from a commutative group. See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Surjective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul ℕ M₂] [Neg M₂] [Sub M₂] [SMul ℤ M₂] [AddCommGroup M₁] (f : M₁ → M₂) (hf : Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddCommGroup M₂

A type endowed with 0 and + is an additive commutative group, if it admits a surjective map that preserves 0 and + to an additive commutative group.