# 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_additive`ized from the versions for `^`.

### Injective #

source
@[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].

Equations

- Function.Injective.semigroup f hf mul = { toMul := inst✝¹, mul_assoc := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

Equations

- Function.Injective.addSemigroup f hf mul = { toAdd := inst✝¹, add_assoc := ⋯ }

Instances For

source
@[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.

Equations

- Function.Injective.commMagma f hf mul = { toMul := inst✝¹, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.addCommMagma {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommMagma M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

Equations

- Function.Injective.addCommMagma f hf mul = { toAdd := inst✝¹, add_comm := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.commSemigroup f hf mul = { toSemigroup := Function.Injective.semigroup f hf mul, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

Equations

- Function.Injective.addCommSemigroup f hf mul = { toAddSemigroup := Function.Injective.addSemigroup f hf mul, add_comm := ⋯ }

Instances For

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

source
theorem Function.Injective.isLeftCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsLeftCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

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

source
theorem Function.Injective.isRightCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsRightCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

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

source
theorem Function.Injective.isCancelAdd {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Add M₂] [IsCancelAdd M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

source
@[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].

Equations

- Function.Injective.leftCancelSemigroup f hf mul = { toSemigroup := Function.Injective.semigroup f hf mul, toIsLeftCancelMul := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.addLeftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddLeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

Equations

- Function.Injective.addLeftCancelSemigroup f hf mul = { toAddSemigroup := Function.Injective.addSemigroup f hf mul, toIsLeftCancelAdd := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.rightCancelSemigroup f hf mul = { toSemigroup := Function.Injective.semigroup f hf mul, toIsRightCancelMul := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.addRightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddRightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f) (add : ∀ (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.

Equations

- Function.Injective.addRightCancelSemigroup f hf mul = { toAddSemigroup := Function.Injective.addSemigroup f hf mul, toIsRightCancelAdd := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.mulOneClass f hf one mul = { toOne := inst✝¹, toMul := inst✝², one_mul := ⋯, mul_one := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (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`.

Equations

- Function.Injective.addZeroClass f hf one mul = { toZero := inst✝¹, toAdd := inst✝², zero_add := ⋯, add_zero := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- Function.Injective.cancelMonoid f hf one mul npow = { toLeftCancelMonoid := Function.Injective.leftCancelMonoid f hf one mul npow, toIsRightCancelMul := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- Function.Injective.addCancelMonoid f hf one mul npow = { toAddLeftCancelMonoid := Function.Injective.addLeftCancelMonoid f hf one mul npow, toIsRightCancelAdd := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.commMonoid f hf one mul npow = { toMonoid := Function.Injective.monoid f hf one mul npow, mul_comm := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- Function.Injective.addCommMonoid f hf one mul npow = { toAddMonoid := Function.Injective.addMonoid f hf one mul npow, add_comm := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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]

Equations

- Function.Injective.involutiveInv f hf inv = { toInv := inst✝¹, inv_inv := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Injective.involutiveNeg {M₂ : Type u_2} {M₁ : Type u_3} [Neg M₁] [InvolutiveNeg M₂] (f : M₁ → M₂) (hf : Injective f) (neg : ∀ (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.

Equations

- Function.Injective.involutiveNeg f hf inv = { toNeg := inst✝¹, neg_neg := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.invOneClass f hf one inv = { toOne := inst✝², toInv := inst✝¹, inv_one := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (neg : ∀ (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`.

Equations

- Function.Injective.negZeroClass f hf one inv = { toZero := inst✝², toNeg := inst✝¹, neg_zero := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- Function.Injective.divInvOneMonoid f hf one mul inv div npow zpow = { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_one := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- Function.Injective.subNegZeroMonoid f hf one mul inv div npow zpow = { toSubNegMonoid := Function.Injective.subNegMonoid f hf one mul inv div npow zpow, neg_zero := ⋯ }

Instances For

source
@[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]

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- Function.Injective.divisionCommMonoid f hf one mul inv div npow zpow = { toDivisionMonoid := Function.Injective.divisionMonoid f hf one mul inv div npow zpow, mul_comm := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- Function.Injective.subtractionCommMonoid f hf one mul inv div npow zpow = { toSubtractionMonoid := Function.Injective.subtractionMonoid f hf one mul inv div npow zpow, add_comm := ⋯ }

Instances For

source
@[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].

Equations

- Function.Injective.group f hf one mul inv div npow zpow = { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_mul_cancel := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- Function.Injective.addGroup f hf one mul inv div npow zpow = { toSubNegMonoid := Function.Injective.subNegMonoid f hf one mul inv div npow zpow, neg_add_cancel := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

### Surjective #

source
@[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].

Equations

- Function.Surjective.semigroup f hf mul = { toMul := inst✝¹, mul_assoc := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Surjective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (add : ∀ (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.

Equations

- Function.Surjective.addSemigroup f hf mul = { toAdd := inst✝¹, add_assoc := ⋯ }

Instances For

source
@[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].

Equations

- Function.Surjective.commMagma f hf mul = { toMul := inst✝¹, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Surjective.addCommMagma {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddCommMagma M₁] (f : M₁ → M₂) (hf : Surjective f) (add : ∀ (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.

Equations

- Function.Surjective.addCommMagma f hf mul = { toAdd := inst✝¹, add_comm := ⋯ }

Instances For

source
@[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].

Equations

- Function.Surjective.commSemigroup f hf mul = { toSemigroup := Function.Surjective.semigroup f hf mul, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Surjective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddCommSemigroup M₁] (f : M₁ → M₂) (hf : Surjective f) (add : ∀ (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.

Equations

- Function.Surjective.addCommSemigroup f hf mul = { toAddSemigroup := Function.Surjective.addSemigroup f hf mul, add_comm := ⋯ }

Instances For

source
@[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].

Equations

- Function.Surjective.mulOneClass f hf one mul = { toOne := inst✝¹, toMul := inst✝², one_mul := ⋯, mul_one := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (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`.

Equations

- Function.Surjective.addZeroClass f hf one mul = { toZero := inst✝¹, toAdd := inst✝², zero_add := ⋯, add_zero := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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]

Equations

- Function.Surjective.involutiveInv f hf inv = { toInv := inst✝¹, inv_inv := ⋯ }

Instances For

source
@[reducible, inline]
abbrev Function.Surjective.involutiveNeg {M₁ : Type u_1} {M₂ : Type u_3} [Neg M₂] [InvolutiveNeg M₁] (f : M₁ → M₂) (hf : Surjective f) (neg : ∀ (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.

Equations

- Function.Surjective.involutiveNeg f hf inv = { toNeg := inst✝¹, neg_neg := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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].

Equations

- Function.Surjective.group f hf one mul inv div npow zpow = { toDivInvMonoid := Function.Surjective.divInvMonoid f hf one mul inv div npow zpow, inv_mul_cancel := ⋯ }

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- Function.Surjective.addGroup f hf one mul inv div npow zpow = { toSubNegMonoid := Function.Surjective.subNegMonoid f hf one mul inv div npow zpow, neg_add_cancel := ⋯ }

Instances For

source
@[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].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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) (zero : f 0 = 0) (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) :
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For