algebra.group.inj_surj - mathlib docs

source

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) :

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

Equations

function.injective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}

source

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) :

add_semigroup M₁

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

source

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

add_comm_semigroup M₁

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

source

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) :

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

Equations

function.injective.comm_semigroup f hf mul = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, mul_comm := _}

source

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

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

Equations

function.injective.left_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_left_cancel := _}

source

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

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

source

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

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

Equations

function.injective.right_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_right_cancel := _}

source

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

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

source

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) :

add_zero_class M₁

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.

source

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) :

mul_one_class M₁

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

function.injective.mul_one_class f hf one mul = {one := 1, mul := has_mul.mul _inst_1, one_mul := _, mul_one := _}

source

def function.injective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero 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) :

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

source

def function.injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one 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) :

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

function.injective.monoid f hf one mul = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, one := mul_one_class.one (function.injective.mul_one_class f hf one mul), one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul M₁), npow_zero' := _, npow_succ' := _}

source

def function.injective.left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [left_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) :

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

Equations

function.injective.left_cancel_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.injective.monoid f hf one mul), npow_zero' := _, npow_succ' := _}

source

def function.injective.add_left_cancel_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [add_left_cancel_monoid M₂] (f : M₁ → M₂) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

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

source

def function.injective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero 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) :

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

source

def function.injective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one 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) :

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

Equations

function.injective.comm_monoid f hf one mul = {mul := comm_semigroup.mul (function.injective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.injective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _}

source

def function.injective.add_cancel_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [add_cancel_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) :

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

source

def function.injective.cancel_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [cancel_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) :

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

Equations

function.injective.cancel_comm_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _}

source

def function.injective.sub_neg_add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [has_neg M₁] [has_sub 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) :

sub_neg_monoid M₁

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.

source

def function.injective.div_inv_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_inv M₁] [has_div 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) :

div_inv_monoid M₁

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

function.injective.div_inv_monoid f hf one mul inv div = {mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.injective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, inv := has_inv.inv _inst_3, div := has_div.div _inst_4, div_eq_mul_inv := _, gpow := gpow_rec {inv := has_inv.inv _inst_3}, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _}

source

def function.injective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_inv M₁] [has_div 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) :

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

function.injective.group f hf one mul inv div = {mul := div_inv_monoid.mul (function.injective.div_inv_monoid f hf one mul inv div), mul_assoc := _, one := div_inv_monoid.one (function.injective.div_inv_monoid f hf one mul inv div), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (function.injective.div_inv_monoid f hf one mul inv div), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (function.injective.div_inv_monoid f hf one mul inv div), div := div_inv_monoid.div (function.injective.div_inv_monoid f hf one mul inv div), div_eq_mul_inv := _, gpow := gpow (function.injective.div_inv_monoid f hf one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}

source

def function.injective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [has_neg M₁] [has_sub 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) :

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

source

def function.injective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₁] [has_one M₁] [has_inv M₁] [has_div 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) :

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

Equations

function.injective.comm_group f hf one mul inv div = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, inv := group.inv (function.injective.group f hf one mul inv div), div := group.div (function.injective.group f hf one mul inv div), div_eq_mul_inv := _, gpow := group.gpow (function.injective.group f hf one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

def function.injective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₁] [has_zero M₁] [has_neg M₁] [has_sub 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) :

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

source

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) :

add_semigroup M₂

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

source

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) :

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

Equations

function.surjective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}

source

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) :

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

Equations

function.surjective.comm_semigroup f hf mul = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, mul_comm := _}

source

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

add_comm_semigroup M₂

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

source

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) :

mul_one_class M₂

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

function.surjective.mul_one_class f hf one mul = {one := 1, mul := has_mul.mul _inst_1, one_mul := _, mul_one := _}

source

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) :

add_zero_class M₂

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.

source

def function.surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one 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) :

monoid M₂

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

Equations

function.surjective.monoid f hf one mul = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, one := mul_one_class.one (function.surjective.mul_one_class f hf one mul), one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul M₂), npow_zero' := _, npow_succ' := _}

source

def function.surjective.add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero 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) :

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

source

def function.surjective.add_comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero 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) :

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

source

def function.surjective.comm_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one 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) :

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

Equations

function.surjective.comm_monoid f hf one mul = {mul := comm_semigroup.mul (function.surjective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.surjective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _}

source

def function.surjective.div_inv_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_inv M₂] [has_div 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) :

div_inv_monoid M₂

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

Equations

function.surjective.div_inv_monoid f hf one mul inv div = {mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.surjective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, inv := has_inv.inv _inst_3, div := has_div.div _inst_4, div_eq_mul_inv := _, gpow := gpow_rec {inv := has_inv.inv _inst_3}, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _}

source

def function.surjective.sub_neg_add_monoid {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [has_neg M₂] [has_sub 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) :

sub_neg_monoid M₂

A type endowed with 0, +, and - (unary and binary) is an additive group, if it admits a surjective map that preserves 0, +, and - from a sub_neg_monoid

source

def function.surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_inv M₂] [has_div 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) :

group M₂

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

Equations

function.surjective.group f hf one mul inv div = {mul := div_inv_monoid.mul (function.surjective.div_inv_monoid f hf one mul inv div), mul_assoc := _, one := div_inv_monoid.one (function.surjective.div_inv_monoid f hf one mul inv div), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (function.surjective.div_inv_monoid f hf one mul inv div), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (function.surjective.div_inv_monoid f hf one mul inv div), div := div_inv_monoid.div (function.surjective.div_inv_monoid f hf one mul inv div), div_eq_mul_inv := _, gpow := gpow (function.surjective.div_inv_monoid f hf one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}

source

def function.surjective.add_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [has_neg M₂] [has_sub 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) :

add_group M₂

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

source

def function.surjective.comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_mul M₂] [has_one M₂] [has_inv M₂] [has_div 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) :

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

Equations

function.surjective.comm_group f hf one mul inv div = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.surjective.comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, inv := group.inv (function.surjective.group f hf one mul inv div), div := group.div (function.surjective.group f hf one mul inv div), div_eq_mul_inv := _, gpow := group.gpow (function.surjective.group f hf one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

def function.surjective.add_comm_group {M₁ : Type u_1} {M₂ : Type u_2} [has_add M₂] [has_zero M₂] [has_neg M₂] [has_sub 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) :

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

mathlib documentation

Lifting algebraic data classes along injective/surjective maps #

Injective #

Surjective #