# mathlib3documentation

algebra.group.inj_surj

# Lifting algebraic data classes along injective/surjective maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 `has_one H`, `has_mul H`, and `has_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.

### Injective #

@[protected, reducible]
def function.injective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [semigroup M₂] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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

Equations
@[protected, reducible]
def function.injective.add_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [add_semigroup M₂] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.injective.add_comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.injective.comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [comm_semigroup M₂] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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].

Equations
@[protected, reducible]
def function.injective.left_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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].

Equations
@[protected, reducible]
def function.injective.add_left_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.injective.right_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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].

Equations
@[protected, reducible]
def function.injective.add_right_cancel_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] (f : M₁ M₂) (hf : function.injective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.injective.add_zero_class {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [add_zero_class M₂] (f : M₁ M₂) (hf : function.injective f) (one : f 0 = 0) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.injective.mul_one_class {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [mul_one_class M₂] (f : M₁ M₂) (hf : function.injective f) (one : f 1 = 1) (mul : (x y : M₁), f (x * y) = f x * f y) :

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

Equations
@[protected, reducible]
def function.injective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [add_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [monoid M₂] (f : M₁ M₂) (hf : function.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].

Equations
@[protected, reducible]
def function.injective.add_monoid_with_one {M₂ : Type u_2} {M₁ : Type u_1} [has_zero M₁] [has_one M₁] [has_add M₁] [ M₁] [has_nat_cast M₁] (f : M₁ M₂) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.injective.left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.add_left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.right_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.add_right_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.add_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [cancel_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [add_comm_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [comm_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.add_comm_monoid_with_one {M₂ : Type u_2} {M₁ : Type u_1} [has_zero M₁] [has_one M₁] [has_add M₁] [ M₁] [has_nat_cast M₁] (f : M₁ M₂) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.injective.add_cancel_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.cancel_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.has_involutive_inv {M₂ : Type u_2} {M₁ : Type u_1} [has_inv M₁] (f : M₁ M₂) (hf : function.injective f) (inv : (x : M₁), f x⁻¹ = (f x)⁻¹) :

A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion.

Equations
@[protected, reducible]
def function.injective.has_involutive_neg {M₂ : Type u_2} {M₁ : Type u_1} [has_neg M₁] (f : M₁ M₂) (hf : function.injective f) (inv : (x : M₁), f (-x) = -f x) :

A type has an involutive negation if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion.

Equations
@[protected, reducible]
def function.injective.sub_neg_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] [sub_neg_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.div_inv_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [has_inv M₁] [has_div M₁] [has_pow M₁ ] [div_inv_monoid M₂] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.subtraction_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.division_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [has_inv M₁] [has_div M₁] [has_pow M₁ ] [division_monoid M₂] (f : M₁ M₂) (hf : function.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) :

A type endowed with `1`, `*`, `⁻¹`, and `/` is a `division_monoid` if it admits an injective map that preserves `1`, `*`, `⁻¹`, and `/` to a `division_monoid`.

Equations
@[protected, reducible]
def function.injective.division_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [has_inv M₁] [has_div M₁] [has_pow M₁ ] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.subtraction_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [has_inv M₁] [has_div M₁] [has_pow M₁ ] [group M₂] (f : M₁ M₂) (hf : function.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].

Equations
@[protected, reducible]
def function.injective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] [add_group M₂] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.injective.add_group_with_one {M₂ : Type u_2} {M₁ : Type u_1} [has_zero M₁] [has_one M₁] [has_add M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] [has_nat_cast M₁] [has_int_cast M₁] (f : M₁ M₂) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (neg : (x : M₁), f (-x) = -f x) (sub : (x y : M₁), f (x - y) = f x - f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (zsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.injective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_pow M₁ ] [has_inv M₁] [has_div M₁] [has_pow M₁ ] [comm_group M₂] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.injective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] [add_comm_group M₂] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.injective.add_comm_group_with_one {M₂ : Type u_2} {M₁ : Type u_1} [has_zero M₁] [has_one M₁] [has_add M₁] [ M₁] [has_neg M₁] [has_sub M₁] [ M₁] [has_nat_cast M₁] [has_int_cast M₁] (f : M₁ M₂) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (neg : (x : M₁), f (-x) = -f x) (sub : (x y : M₁), f (x - y) = f x - f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (zsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

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

Equations

### Surjective #

@[protected, reducible]
def function.surjective.add_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [add_semigroup M₁] (f : M₁ M₂) (hf : function.surjective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.surjective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [semigroup M₁] (f : M₁ M₂) (hf : function.surjective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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

Equations
@[protected, reducible]
def function.surjective.comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [comm_semigroup M₁] (f : M₁ M₂) (hf : function.surjective f) (mul : (x y : M₁), f (x * y) = f x * f y) :

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].

Equations
@[protected, reducible]
def function.surjective.add_comm_semigroup {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] (f : M₁ M₂) (hf : function.surjective f) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.surjective.mul_one_class {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [mul_one_class M₁] (f : M₁ M₂) (hf : function.surjective f) (one : f 1 = 1) (mul : (x y : M₁), f (x * y) = f x * f y) :

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

Equations
@[protected, reducible]
def function.surjective.add_zero_class {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [add_zero_class M₁] (f : M₁ M₂) (hf : function.surjective f) (one : f 0 = 0) (mul : (x y : M₁), f (x + y) = f x + f y) :

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

Equations
@[protected, reducible]
def function.surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_pow M₂ ] [monoid M₁] (f : M₁ M₂) (hf : function.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].

Equations
@[protected, reducible]
def function.surjective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [ M₂] [add_monoid M₁] (f : M₁ M₂) (hf : function.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) :

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 `[has_smul ℕ M₂]` argument.

Equations
@[protected, reducible]
def function.surjective.add_monoid_with_one {M₁ : Type u_1} {M₂ : Type u_2} [has_zero M₂] [has_one M₂] [has_add M₂] [ M₂] [has_nat_cast M₂] (f : M₁ M₂) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.surjective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [ M₂] [add_comm_monoid M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.surjective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_pow M₂ ] [comm_monoid M₁] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.surjective.add_comm_monoid_with_one {M₁ : Type u_1} {M₂ : Type u_2} [has_zero M₂] [has_one M₂] [has_add M₂] [ M₂] [has_nat_cast M₂] (f : M₁ M₂) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) :

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

Equations
@[protected, reducible]
def function.surjective.has_involutive_inv {M₁ : Type u_1} {M₂ : Type u_2} [has_inv M₂] (f : M₁ M₂) (hf : function.surjective f) (inv : (x : M₁), f x⁻¹ = (f x)⁻¹) :

A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion.

Equations
@[protected, reducible]
def function.surjective.has_involutive_neg {M₁ : Type u_1} {M₂ : Type u_2} [has_neg M₂] (f : M₁ M₂) (hf : function.surjective f) (inv : (x : M₁), f (-x) = -f x) :

A type has an involutive negation if it admits a surjective map that preserves `⁻¹` to a type which has an involutive inversion.

Equations
@[protected, reducible]
def function.surjective.div_inv_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_pow M₂ ] [has_inv M₂] [has_div M₂] [has_pow M₂ ] [div_inv_monoid M₁] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.surjective.sub_neg_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [ M₂] [has_neg M₂] [has_sub M₂] [ M₂] [sub_neg_monoid M₁] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_pow M₂ ] [has_inv M₂] [has_div M₂] [has_pow M₂ ] [group M₁] (f : M₁ M₂) (hf : function.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].

Equations
@[protected, reducible]
def function.surjective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [ M₂] [has_neg M₂] [has_sub M₂] [ M₂] [add_group M₁] (f : M₁ M₂) (hf : function.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) :

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

Equations
@[protected, reducible]
def function.surjective.add_group_with_one {M₁ : Type u_1} {M₂ : Type u_2} [has_zero M₂] [has_one M₂] [has_add M₂] [has_neg M₂] [has_sub M₂] [ M₂] [ M₂] [has_nat_cast M₂] [has_int_cast M₂] (f : M₁ M₂) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (neg : (x : M₁), f (-x) = -f x) (sub : (x y : M₁), f (x - y) = f x - f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (zsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

A type endowed with `0`, `1`, `+` is an additive group with one, if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_pow M₂ ] [has_inv M₂] [has_div M₂] [has_pow M₂ ] [comm_group M₁] (f : M₁ M₂) (hf : function.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) :

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].

Equations
@[protected, reducible]
def function.surjective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [ M₂] [has_neg M₂] [has_sub M₂] [ M₂] [add_comm_group M₁] (f : M₁ M₂) (hf : function.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) :

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.

Equations
@[protected, reducible]
def function.surjective.add_comm_group_with_one {M₁ : Type u_1} {M₂ : Type u_2} [has_zero M₂] [has_one M₂] [has_add M₂] [has_neg M₂] [has_sub M₂] [ M₂] [ M₂] [has_nat_cast M₂] [has_int_cast M₂] (f : M₁ M₂) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : M₁), f (x + y) = f x + f y) (neg : (x : M₁), f (-x) = -f x) (sub : (x y : M₁), f (x - y) = f x - f y) (nsmul : (x : M₁) (n : ), f (n x) = n f x) (zsmul : (x : M₁) (n : ), f (n x) = n f x) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

A type endowed with `0`, `1`, `+` is an additive commutative group with one, if it admits a surjective map that preserves `0`, `1`, and `+` to an additive commutative group with one. See note [reducible non-instances].

Equations