Documentation

Mathlib.Algebra.Hom.Equiv.Basic

Multiplicative and additive equivs #

In this file we define two extensions of Equiv called AddEquiv and MulEquiv, which are datatypes representing isomorphisms of AddMonoids/AddGroups and Monoids/Groups.

Notations #

The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.

Tags #

Equiv, MulEquiv, AddEquiv

def AddHom.inverse {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
AddHom N M

Makes an additive inverse from a bijection which preserves addition.

Equations
  • AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := (_ : ∀ (x y : N), g (x + y) = g x + g y) }
def AddHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (x : N) (y : N) :
g (x + y) = g x + g y
Equations
  • (_ : g (x + y) = g x + g y) = (_ : g (x + y) = g x + g y)
def MulHom.inverse {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations
  • MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := (_ : ∀ (x y : N), g (x * y) = g x * g y) }
def AddMonoidHom.inverse.proof_2 {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (x : B) (y : B) :
AddHom.toFun (AddHom.inverse (f) g h₁ h₂) (x + y) = AddHom.toFun (AddHom.inverse (f) g h₁ h₂) x + AddHom.toFun (AddHom.inverse (f) g h₁ h₂) y
Equations
  • One or more equations did not get rendered due to their size.
def AddMonoidHom.inverse.proof_1 {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) :
g 0 = 0
Equations
  • (_ : g 0 = 0) = (_ : g 0 = 0)
def AddMonoidHom.inverse {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
B →+ A

The inverse of a bijective AddMonoidHom is an AddMonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MonoidHom.inverse_apply {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst : Monoid B] (f : A →* B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
∀ (a : B), ↑(MonoidHom.inverse f g h₁ h₂) a = g a
@[simp]
theorem AddMonoidHom.inverse_apply {A : Type u_1} {B : Type u_2} [inst : AddMonoid A] [inst : AddMonoid B] (f : A →+ B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
∀ (a : B), ↑(AddMonoidHom.inverse f g h₁ h₂) a = g a
def MonoidHom.inverse {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst : Monoid B] (f : A →* B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
B →* A

The inverse of a bijective MonoidHom is a MonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
structure AddEquiv (A : Type u_1) (B : Type u_2) [inst : Add A] [inst : Add B] extends Equiv :
Type (maxu_1u_2)

AddEquiv α β is the type of an equiv α ≃ β≃ β which preserves addition.

Instances For
    class AddEquivClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [inst : Add A] [inst : Add B] extends EquivLike :
    Type (max(maxu_1u_2)u_3)
    • Preserves addition.

      map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b

    AddEquivClass F A B states that F is a type of addition-preserving morphisms. You should extend this class when you extend AddEquiv.

    Instances
      abbrev AddEquiv.toAddHom {A : Type u_1} {B : Type u_2} [inst : Add A] [inst : Add B] (self : A ≃+ B) :
      AddHom A B

      The AddHom underlying a AddEquiv.

      Equations
      structure MulEquiv (M : Type u_1) (N : Type u_2) [inst : Mul M] [inst : Mul N] extends Equiv :
      Type (maxu_1u_2)

      MulEquiv α β is the type of an equiv α ≃ β≃ β which preserves multiplication.

      Instances For
        abbrev MulEquiv.toMulHom {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (self : M ≃* N) :

        The MulHom underlying a MulEquiv.

        Equations
        class MulEquivClass (F : Type u_1) (A : outParam (Type u_2)) (B : outParam (Type u_3)) [inst : Mul A] [inst : Mul B] extends EquivLike :
        Type (max(maxu_1u_2)u_3)
        • Preserves multiplication.

          map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b

        MulEquivClass F A B states that F is a type of multiplication-preserving morphisms. You should extend this class when you extend MulEquiv.

        Instances
          instance AddEquivClass.instAddHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          {x : Add M} → {x_1 : Add N} → [h : AddEquivClass F M N] → AddHomClass F M N
          Equations
          def AddEquivClass.instAddHomClass.proof_1 (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          ∀ {x : Add M} {x_1 : Add N} [h : AddEquivClass F M N], Function.Injective FunLike.coe
          Equations
          instance MulEquivClass.instMulHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          {x : Mul M} → {x_1 : Mul N} → [h : MulEquivClass F M N] → MulHomClass F M N
          Equations
          instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          {x : AddZeroClass M} → {x_1 : AddZeroClass N} → [inst : AddEquivClass F M N] → AddMonoidHomClass F M N
          Equations
          def AddEquivClass.instAddMonoidHomClass.proof_2 (F : Type u_3) {M : Type u_2} {N : Type u_1} :
          ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N] (f : F) (x_2 y : M), f (x_2 + y) = f x_2 + f y
          Equations
          • (_ : ∀ (f : F) (x y : M), f (x + y) = f x + f y) = (_ : ∀ (f : F) (x y : M), f (x + y) = f x + f y)
          def AddEquivClass.instAddMonoidHomClass.proof_1 (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N], Function.Injective FunLike.coe
          Equations
          def AddEquivClass.instAddMonoidHomClass.proof_3 (F : Type u_2) {M : Type u_3} {N : Type u_1} :
          ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} [inst : AddEquivClass F M N] (e : F), e 0 = 0
          Equations
          • (_ : e 0 = 0) = (_ : e 0 = 0)
          instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_2} {N : Type u_3} :
          {x : MulOneClass M} → {x_1 : MulOneClass N} → [inst : MulEquivClass F M N] → MonoidHomClass F M N
          Equations
          instance MulEquivClass.toMonoidWithZeroHomClass (F : Type u_1) {α : Type u_2} {β : Type u_3} :
          {x : MulZeroOneClass α} → {x_1 : MulZeroOneClass β} → [inst : MulEquivClass F α β] → MonoidWithZeroHomClass F α β
          Equations
          @[simp]
          theorem AddEquivClass.map_eq_zero_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddEquivClass F M N] (h : F) {x : M} :
          h x = 0 x = 0
          @[simp]
          theorem MulEquivClass.map_eq_one_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulEquivClass F M N] (h : F) {x : M} :
          h x = 1 x = 1
          theorem AddEquivClass.map_ne_zero_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddEquivClass F M N] (h : F) {x : M} :
          h x 0 x 0
          theorem MulEquivClass.map_ne_one_iff {F : Type u_3} {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulEquivClass F M N] (h : F) {x : M} :
          h x 1 x 1
          def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst : Add β] [inst : AddEquivClass F α β] (f : F) :
          α ≃+ β

          Turn an element of a type F satisfying AddEquivClass F α β into an actual AddEquiv. This is declared as the default coercion from F to α ≃+ β≃+ β.

          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Mul β] [inst : MulEquivClass F α β] (f : F) :
          α ≃* β

          Turn an element of a type F satisfying MulEquivClass F α β into an actual MulEquiv. This is declared as the default coercion from F to α ≃* β≃* β.

          Equations
          • One or more equations did not get rendered due to their size.
          instance instCoeTCAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst : Add β] [inst : AddEquivClass F α β] :
          CoeTC F (α ≃+ β)

          Any type satisfying AddEquivClass can be cast into AddEquiv via AddEquivClass.toAddEquiv.

          Equations
          • instCoeTCAddEquiv = { coe := AddEquivClass.toAddEquiv }
          instance instCoeTCMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Mul β] [inst : MulEquivClass F α β] :
          CoeTC F (α ≃* β)

          Any type satisfying MulEquivClass can be cast into MulEquiv via MulEquivClass.toMulEquiv.

          Equations
          • instCoeTCMulEquiv = { coe := MulEquivClass.toMulEquiv }
          def AddEquiv.instAddEquivClassAddEquiv.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) (g : M ≃+ N) (h₁ : (fun f => f.toEquiv.toFun) f = (fun f => f.toEquiv.toFun) g) (h₂ : (fun f => f.toEquiv.invFun) f = (fun f => f.toEquiv.invFun) g) :
          f = g
          Equations
          • (_ : f = g) = (_ : f = g)
          instance AddEquiv.instAddEquivClassAddEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :
          Equations
          def AddEquiv.instAddEquivClassAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun
          Equations
          def AddEquiv.instAddEquivClassAddEquiv.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun
          Equations
          instance MulEquiv.instMulEquivClassMulEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :
          Equations
          @[simp]
          theorem AddEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          f.toEquiv = f
          @[simp]
          theorem MulEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          f.toEquiv = f
          @[simp]
          theorem AddEquiv.coe_toEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          f = f
          @[simp]
          theorem MulEquiv.coe_toEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          f = f
          @[simp]
          theorem AddEquiv.coe_toAddHom {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} :
          ↑(AddEquiv.toAddHom f) = f
          @[simp]
          theorem MulEquiv.coe_toMulHom {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} :
          ↑(MulEquiv.toMulHom f) = f
          theorem AddEquiv.map_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) (x : M) (y : M) :
          f (x + y) = f x + f y

          An additive isomorphism preserves addition.

          theorem MulEquiv.map_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) (x : M) (y : M) :
          f (x * y) = f x * f y

          A multiplicative isomorphism preserves multiplication.

          def AddEquiv.mk' {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M N) (h : ∀ (x y : M), f (x + y) = f x + f y) :
          M ≃+ N

          Makes an additive isomorphism from a bijection which preserves addition.

          Equations
          def MulEquiv.mk' {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M N) (h : ∀ (x y : M), f (x * y) = f x * f y) :
          M ≃* N

          Makes a multiplicative isomorphism from a bijection which preserves multiplication.

          Equations
          theorem AddEquiv.bijective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          theorem MulEquiv.bijective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          theorem AddEquiv.injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          theorem MulEquiv.injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          theorem AddEquiv.surjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          theorem MulEquiv.surjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          def AddEquiv.refl (M : Type u_1) [inst : Add M] :
          M ≃+ M

          The identity map is an additive isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.refl.proof_1 (M : Type u_1) [inst : Add M] :
          ∀ (x x_1 : M), Equiv.toFun { toFun := (Equiv.refl M).toFun, invFun := (Equiv.refl M).invFun, left_inv := (_ : Function.LeftInverse (Equiv.refl M).invFun (Equiv.refl M).toFun), right_inv := (_ : Function.RightInverse (Equiv.refl M).invFun (Equiv.refl M).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.refl M).toFun, invFun := (Equiv.refl M).invFun, left_inv := (_ : Function.LeftInverse (Equiv.refl M).invFun (Equiv.refl M).toFun), right_inv := (_ : Function.RightInverse (Equiv.refl M).invFun (Equiv.refl M).toFun) } (x + x_1)
          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquiv.refl (M : Type u_1) [inst : Mul M] :
          M ≃* M

          The identity map is a multiplicative isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          instance AddEquiv.instInhabitedAddEquiv {M : Type u_1} [inst : Add M] :
          Equations
          instance MulEquiv.instInhabitedMulEquiv {M : Type u_1} [inst : Mul M] :
          Equations
          def AddEquiv.symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (h : M ≃+ N) :
          N ≃+ M

          The inverse of an isomorphism is an isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.symm.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (h : M ≃+ N) (a : N) (b : N) :
          ↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) (a + b) = ↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) a + ↑(AddHom.inverse (AddEquiv.toAddHom h) ↑(Equiv.symm h.toEquiv) (_ : Function.LeftInverse h.toEquiv.invFun h.toEquiv.toFun) (_ : Function.RightInverse h.toEquiv.invFun h.toEquiv.toFun)) b
          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquiv.symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (h : M ≃* N) :
          N ≃* M

          The inverse of an isomorphism is an isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem AddEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} :
          f.toEquiv.invFun = ↑(AddEquiv.symm f)
          theorem MulEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} :
          f.toEquiv.invFun = ↑(MulEquiv.symm f)
          @[simp]
          theorem AddEquiv.coe_toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          ↑(Equiv.symm f) = ↑(AddEquiv.symm f)
          @[simp]
          theorem MulEquiv.coe_toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          ↑(Equiv.symm f) = ↑(MulEquiv.symm f)
          @[simp]
          theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          @[simp]
          theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          def AddEquiv.Simps.symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          NM

          See Note [custom simps projection]

          Equations
          def MulEquiv.Simps.symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          NM

          See Note [custom simps projection]

          Equations
          @[simp]
          theorem AddEquiv.toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          @[simp]
          theorem MulEquiv.toEquiv_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          @[simp]
          theorem AddEquiv.coe_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
          { toEquiv := f, map_add' := hf } = f
          @[simp]
          theorem MulEquiv.coe_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
          { toEquiv := f, map_mul' := hf } = f
          @[simp]
          theorem AddEquiv.symm_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
          @[simp]
          theorem MulEquiv.symm_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
          theorem AddEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :
          Function.Bijective AddEquiv.symm
          theorem MulEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :
          Function.Bijective MulEquiv.symm
          @[simp]
          theorem AddEquiv.symm_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M N) (h : ∀ (x y : M), Equiv.toFun f (x + y) = Equiv.toFun f x + Equiv.toFun f y) :
          AddEquiv.symm { toEquiv := f, map_add' := h } = { toEquiv := Equiv.symm f, map_add' := (_ : ∀ (x y : N), Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv (x + y) = Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv x + Equiv.toFun (AddEquiv.symm { toEquiv := f, map_add' := h }).toEquiv y) }
          @[simp]
          theorem MulEquiv.symm_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M N) (h : ∀ (x y : M), Equiv.toFun f (x * y) = Equiv.toFun f x * Equiv.toFun f y) :
          MulEquiv.symm { toEquiv := f, map_mul' := h } = { toEquiv := Equiv.symm f, map_mul' := (_ : ∀ (x y : N), Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv (x * y) = Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv x * Equiv.toFun (MulEquiv.symm { toEquiv := f, map_mul' := h }).toEquiv y) }
          @[simp]
          @[simp]
          def AddEquiv.trans.proof_1 {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) (x : M) (y : M) :
          h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y)
          Equations
          • (_ : h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y)) = (_ : h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y))
          def AddEquiv.trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
          M ≃+ P

          Transitivity of addition-preserving isomorphisms

          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquiv.trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
          M ≃* P

          Transitivity of multiplication-preserving isomorphisms

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (y : N) :
          e (↑(AddEquiv.symm e) y) = y

          e.symm is a right inverse of e, written as e (e.symm y) = y.

          @[simp]
          theorem MulEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (y : N) :
          e (↑(MulEquiv.symm e) y) = y

          e.symm is a right inverse of e, written as e (e.symm y) = y.

          @[simp]
          theorem AddEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (x : M) :
          ↑(AddEquiv.symm e) (e x) = x

          e.symm is a left inverse of e, written as e.symm (e y) = y.

          @[simp]
          theorem MulEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (x : M) :
          ↑(MulEquiv.symm e) (e x) = x

          e.symm is a left inverse of e, written as e.symm (e y) = y.

          @[simp]
          theorem AddEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          ↑(AddEquiv.symm e) e = id
          @[simp]
          theorem MulEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          ↑(MulEquiv.symm e) e = id
          @[simp]
          theorem AddEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          e ↑(AddEquiv.symm e) = id
          @[simp]
          theorem MulEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          e ↑(MulEquiv.symm e) = id
          @[simp]
          theorem AddEquiv.coe_refl {M : Type u_1} [inst : Add M] :
          ↑(AddEquiv.refl M) = id
          @[simp]
          theorem MulEquiv.coe_refl {M : Type u_1} [inst : Mul M] :
          ↑(MulEquiv.refl M) = id
          @[simp]
          theorem AddEquiv.refl_apply {M : Type u_1} [inst : Add M] (m : M) :
          ↑(AddEquiv.refl M) m = m
          @[simp]
          theorem MulEquiv.refl_apply {M : Type u_1} [inst : Mul M] (m : M) :
          ↑(MulEquiv.refl M) m = m
          @[simp]
          theorem AddEquiv.coe_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
          ↑(AddEquiv.trans e₁ e₂) = e₂ e₁
          @[simp]
          theorem MulEquiv.coe_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
          ↑(MulEquiv.trans e₁ e₂) = e₂ e₁
          @[simp]
          theorem AddEquiv.trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
          ↑(AddEquiv.trans e₁ e₂) m = e₂ (e₁ m)
          @[simp]
          theorem MulEquiv.trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
          ↑(MulEquiv.trans e₁ e₂) m = e₂ (e₁ m)
          @[simp]
          theorem AddEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
          ↑(AddEquiv.symm (AddEquiv.trans e₁ e₂)) p = ↑(AddEquiv.symm e₁) (↑(AddEquiv.symm e₂) p)
          @[simp]
          theorem MulEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
          ↑(MulEquiv.symm (MulEquiv.trans e₁ e₂)) p = ↑(MulEquiv.symm e₁) (↑(MulEquiv.symm e₂) p)
          theorem AddEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : M} {y : M} :
          e x = e y x = y
          theorem MulEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : M} {y : M} :
          e x = e y x = y
          theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : M} {y : N} :
          e x = y x = ↑(AddEquiv.symm e) y
          theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : M} {y : N} :
          e x = y x = ↑(MulEquiv.symm e) y
          theorem AddEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : N} {y : M} :
          ↑(AddEquiv.symm e) x = y x = e y
          theorem MulEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : N} {y : (fun x => M) x} :
          ↑(MulEquiv.symm e) x = y x = e y
          theorem AddEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) {x : N} {y : M} :
          y = ↑(AddEquiv.symm e) x e y = x
          theorem MulEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) {x : N} {y : (fun x => M) x} :
          y = ↑(MulEquiv.symm e) x e y = x
          theorem AddEquiv.eq_comp_symm {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : Nα) (g : Mα) :
          f = g ↑(AddEquiv.symm e) f e = g
          theorem MulEquiv.eq_comp_symm {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : Nα) (g : Mα) :
          f = g ↑(MulEquiv.symm e) f e = g
          theorem AddEquiv.comp_symm_eq {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : Nα) (g : Mα) :
          g ↑(AddEquiv.symm e) = f g = f e
          theorem MulEquiv.comp_symm_eq {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : Nα) (g : Mα) :
          g ↑(MulEquiv.symm e) = f g = f e
          theorem AddEquiv.eq_symm_comp {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : αM) (g : αN) :
          f = ↑(AddEquiv.symm e) g e f = g
          theorem MulEquiv.eq_symm_comp {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : αM) (g : αN) :
          f = ↑(MulEquiv.symm e) g e f = g
          theorem AddEquiv.symm_comp_eq {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {α : Type u_1} (e : M ≃+ N) (f : αM) (g : αN) :
          ↑(AddEquiv.symm e) g = f g = e f
          theorem MulEquiv.symm_comp_eq {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {α : Type u_1} (e : M ≃* N) (f : αM) (g : αN) :
          ↑(MulEquiv.symm e) g = f g = e f
          @[simp]
          theorem AddEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          @[simp]
          theorem MulEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          @[simp]
          theorem AddEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) :
          @[simp]
          theorem MulEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) :
          theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
          ↑(AddEquiv.trans e₁ e₂) = AddMonoidHom.comp e₂ e₁
          theorem MulEquiv.coe_monoidHom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
          ↑(MulEquiv.trans e₁ e₂) = MonoidHom.comp e₂ e₁
          theorem AddEquiv.ext {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} (h : ∀ (x : M), f x = g x) :
          f = g

          Two additive isomorphisms agree if they are defined by the same underlying function.

          theorem MulEquiv.ext {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} (h : ∀ (x : M), f x = g x) :
          f = g

          Two multiplicative isomorphisms agree if they are defined by the same underlying function.

          theorem AddEquiv.ext_iff {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} :
          f = g ∀ (x : M), f x = g x
          theorem MulEquiv.ext_iff {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} :
          f = g ∀ (x : M), f x = g x
          @[simp]
          theorem AddEquiv.mk_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (e' : NM) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :
          { toEquiv := { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = e
          @[simp]
          theorem MulEquiv.mk_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (e' : NM) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :
          { toEquiv := { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = e
          @[simp]
          theorem AddEquiv.mk_coe' {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (f : NM) (h₁ : Function.LeftInverse (e) f) (h₂ : Function.RightInverse (e) f) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } y) :
          { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = AddEquiv.symm e
          @[simp]
          theorem MulEquiv.mk_coe' {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (f : NM) (h₁ : Function.LeftInverse (e) f) (h₂ : Function.RightInverse (e) f) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } y) :
          { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = MulEquiv.symm e
          theorem AddEquiv.congr_arg {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {x : M} {x' : M} :
          x = x'f x = f x'
          theorem MulEquiv.congr_arg {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {x : M} {x' : M} :
          x = x'f x = f x'
          theorem AddEquiv.congr_fun {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {g : M ≃+ N} (h : f = g) (x : M) :
          f x = g x
          theorem MulEquiv.congr_fun {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {g : M ≃* N} (h : f = g) (x : M) :
          f x = g x
          def AddEquiv.addEquivOfUnique {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :
          M ≃+ N

          The AddEquiv between two AddMonoids with a unique element.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.addEquivOfUnique.proof_1 {M : Type u_2} {N : Type u_1} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :
          ∀ (x x_1 : M), Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } x + Equiv.toFun { toFun := (Equiv.equivOfUnique M N).toFun, invFun := (Equiv.equivOfUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.equivOfUnique M N).invFun (Equiv.equivOfUnique M N).toFun) } x_1
          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquiv.mulEquivOfUnique {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Mul M] [inst : Mul N] :
          M ≃* N

          The MulEquiv between two monoids with a unique element.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.instUniqueAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :
          ∀ (x : M ≃+ N), x = default
          Equations
          • (_ : x = default) = (_ : x = default)
          instance AddEquiv.instUniqueAddEquiv {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Add N] :
          Unique (M ≃+ N)

          There is a unique additive monoid homomorphism between two additive monoids with a unique element.

          Equations
          • AddEquiv.instUniqueAddEquiv = { toInhabited := { default := AddEquiv.addEquivOfUnique }, uniq := (_ : ∀ (x : M ≃+ N), x = default) }
          instance MulEquiv.instUniqueMulEquiv {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Mul M] [inst : Mul N] :
          Unique (M ≃* N)

          There is a unique monoid homomorphism between two monoids with a unique element.

          Equations
          • MulEquiv.instUniqueMulEquiv = { toInhabited := { default := MulEquiv.mulEquivOfUnique }, uniq := (_ : ∀ (x : M ≃* N), x = default) }

          Monoids #

          theorem AddEquiv.map_zero {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) :
          h 0 = 0

          An additive isomorphism of additive monoids sends 0 to 0 (and is hence an additive monoid isomorphism).

          theorem MulEquiv.map_one {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) :
          h 1 = 1

          A multiplicative isomorphism of monoids sends 1 to 1 (and is hence a monoid isomorphism).

          theorem AddEquiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) {x : M} :
          h x = 0 x = 0
          theorem MulEquiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) {x : M} :
          h x = 1 x = 1
          theorem AddEquiv.map_ne_zero_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) {x : M} :
          h x 0 x 0
          theorem MulEquiv.map_ne_one_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) {x : M} :
          h x 1 x 1
          noncomputable def AddEquiv.ofBijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) (hf : Function.Bijective f) :
          M ≃+ N

          A bijective AddSemigroup homomorphism is an isomorphism

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.ofBijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Add M] [inst : Add N] [inst : AddHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
          ↑(AddEquiv.ofBijective f hf) a = f a
          @[simp]
          theorem MulEquiv.ofBijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) (hf : Function.Bijective f) (a : M) :
          ↑(MulEquiv.ofBijective f hf) a = f a
          noncomputable def MulEquiv.ofBijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [inst : Mul M] [inst : Mul N] [inst : MulHomClass F M N] (f : F) (hf : Function.Bijective f) :
          M ≃* N

          A bijective Semigroup homomorphism is an isomorphism

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective f) :
          f (↑(Equiv.symm (Equiv.ofBijective (f) hf)) n) = n
          @[simp]
          theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective f) :
          f (↑(Equiv.symm (Equiv.ofBijective (f) hf)) n) = n
          def AddEquiv.toAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) :
          M →+ N

          Extract the forward direction of an additive equivalence as an addition-preserving function.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (h : M ≃+ N) (x : M) (y : M) :
          Equiv.toFun h.toEquiv (x + y) = Equiv.toFun h.toEquiv x + Equiv.toFun h.toEquiv y
          Equations
          • One or more equations did not get rendered due to their size.
          def MulEquiv.toMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (h : M ≃* N) :
          M →* N

          Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.coe_toAddMonoidHom {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (e : M ≃+ N) :
          @[simp]
          theorem MulEquiv.coe_toMonoidHom {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (e : M ≃* N) :
          theorem AddEquiv.toAddMonoidHom_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
          Function.Injective AddEquiv.toAddMonoidHom
          theorem MulEquiv.toMonoidHom_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
          Function.Injective MulEquiv.toMonoidHom
          def AddEquiv.arrowCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Add P] [inst : Add Q] (f : M N) (g : P ≃+ Q) :
          (MP) ≃+ (NQ)

          An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.arrowCongr.proof_1 {M : Type u_1} {N : Type u_4} {P : Type u_2} {Q : Type u_3} [inst : Add P] [inst : Add Q] (f : M N) (g : P ≃+ Q) (h : MP) :
          (fun k m => ↑(AddEquiv.symm g) (k (f m))) ((fun h n => g (h (↑(Equiv.symm f) n))) h) = h
          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.arrowCongr.proof_3 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [inst : Add P] [inst : Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (k : MP) :
          Equiv.toFun { toFun := fun h n => g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (f m)), left_inv := (_ : ∀ (h : MP), (fun k m => ↑(AddEquiv.symm g) (k (f m))) ((fun h n => g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun h n => g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (f m))) k) = k) } (h + k) = Equiv.toFun { toFun := fun h n => g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (f m)), left_inv := (_ : ∀ (h : MP), (fun k m => ↑(AddEquiv.symm g) (k (f m))) ((fun h n => g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun h n => g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (f m))) k) = k) } h + Equiv.toFun { toFun := fun h n => g (h (↑(Equiv.symm f) n)), invFun := fun k m => ↑(AddEquiv.symm g) (k (f m)), left_inv := (_ : ∀ (h : MP), (fun k m => ↑(AddEquiv.symm g) (k (f m))) ((fun h n => g (h (↑(Equiv.symm f) n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun h n => g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (f m))) k) = k) } k
          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.arrowCongr.proof_2 {M : Type u_4} {N : Type u_1} {P : Type u_3} {Q : Type u_2} [inst : Add P] [inst : Add Q] (f : M N) (g : P ≃+ Q) (k : NQ) :
          (fun h n => g (h (↑(Equiv.symm f) n))) ((fun k m => ↑(AddEquiv.symm g) (k (f m))) k) = k
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem MulEquiv.arrowCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Mul P] [inst : Mul Q] (f : M N) (g : P ≃* Q) (h : MP) (n : N) :
          ↑(MulEquiv.arrowCongr f g) h n = g (h (↑(Equiv.symm f) n))
          @[simp]
          theorem AddEquiv.arrowCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Add P] [inst : Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (n : N) :
          ↑(AddEquiv.arrowCongr f g) h n = g (h (↑(Equiv.symm f) n))
          def MulEquiv.arrowCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : Mul P] [inst : Mul Q] (f : M N) (g : P ≃* Q) :
          (MP) ≃* (NQ)

          A multiplicative analogue of Equiv.arrowCongr, where the equivalence between the targets is multiplicative.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.addMonoidHomCongr.proof_3 {M : Type u_1} {N : Type u_3} {P : Type u_2} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) (k : M →+ P) :
          Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } (h + k) = Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } h + Equiv.toFun { toFun := fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := (_ : ∀ (h : M →+ P), (fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun h => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun k => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k) } k
          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.addMonoidHomCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) :
          (M →+ P) ≃+ (N →+ Q)

          An additive analogue of Equiv.arrowCongr, for additive maps from an additive monoid to a commutative additive monoid.

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem MulEquiv.monoidHomCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] [inst : CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
          @[simp]
          theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] [inst : AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
          def MulEquiv.monoidHomCongr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] [inst : CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) :
          (M →* P) ≃* (N →* Q)

          A multiplicative analogue of Equiv.arrowCongr, for multiplicative maps from a monoid to a commutative monoid.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.piCongrRight {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
          ((j : η) → Ms j) ≃+ ((j : η) → Ns j)

          A family of additive equivalences Π j, (Ms j ≃+ Ns j)≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j.

          This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.piCongrRight.proof_3 {η : Type u_1} {Ms : ηType u_3} {Ns : ηType u_2} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (y : (j : η) → Ms j) :
          Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } (x + y) = Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } x + Equiv.toFun { toFun := fun x j => ↑(es j) (x j), invFun := fun x j => ↑(AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun) } y
          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.piCongrRight.proof_2 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
          Function.RightInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun
          Equations
          • One or more equations did not get rendered due to their size.
          def AddEquiv.piCongrRight.proof_1 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
          Function.LeftInverse (Equiv.piCongrRight fun j => (es j).toEquiv).invFun (Equiv.piCongrRight fun j => (es j).toEquiv).toFun
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.piCongrRight_apply {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
          ↑(AddEquiv.piCongrRight es) x j = ↑(es j) (x j)
          @[simp]
          theorem MulEquiv.piCongrRight_apply {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
          ↑(MulEquiv.piCongrRight es) x j = ↑(es j) (x j)
          def MulEquiv.piCongrRight {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
          ((j : η) → Ms j) ≃* ((j : η) → Ns j)

          A family of multiplicative equivalences Π j, (Ms j ≃* Ns j)≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j.

          This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddEquiv.piCongrRight_refl {η : Type u_1} {Ms : ηType u_2} [inst : (j : η) → Add (Ms j)] :
          (AddEquiv.piCongrRight fun j => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
          @[simp]
          theorem MulEquiv.piCongrRight_refl {η : Type u_1} {Ms : ηType u_2} [inst : (j : η) → Mul (Ms j)] :
          (MulEquiv.piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
          @[simp]
          theorem AddEquiv.piCongrRight_symm {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
          @[simp]
          theorem MulEquiv.piCongrRight_symm {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
          @[simp]
          theorem AddEquiv.piCongrRight_trans {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} {Ps : ηType u_4} [inst : (j : η) → Add (Ms j)] [inst : (j : η) → Add (Ns j)] [inst : (j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
          @[simp]
          theorem MulEquiv.piCongrRight_trans {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} {Ps : ηType u_4} [inst : (j : η) → Mul (Ms j)] [inst : (j : η) → Mul (Ns j)] [inst : (j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
          def AddEquiv.piSubsingleton.proof_1 {ι : Type u_1} (M : ιType u_2) [inst : Subsingleton ι] (i : ι) :
          Equations
          def AddEquiv.piSubsingleton.proof_3 {ι : Type u_2} (M : ιType u_1) [inst : (j : ι) → Add (M j)] (i : ι) :
          ∀ (x x_1 : (j : ι) → M j), (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x_1 i = x i + x_1 i
          Equations
          def AddEquiv.piSubsingleton {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) :
          ((j : ι) → M j) ≃+ M i

          A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem MulEquiv.piSubsingleton_apply {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) (f : (x : ι) → M x) :
          ↑(MulEquiv.piSubsingleton M i) f = f i
          @[simp]
          theorem AddEquiv.piSubsingleton_symm_apply {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) (x : M i) (b : ι) :
          ↑(AddEquiv.symm (AddEquiv.piSubsingleton M i)) x b = cast (_ : M i = M b) x
          @[simp]
          theorem MulEquiv.piSubsingleton_symm_apply {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) (x : M i) (b : ι) :
          ↑(MulEquiv.symm (MulEquiv.piSubsingleton M i)) x b = cast (_ : M i = M b) x
          @[simp]
          theorem AddEquiv.piSubsingleton_apply {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Add (M j)] [inst : Subsingleton ι] (i : ι) (f : (x : ι) → M x) :
          ↑(AddEquiv.piSubsingleton M i) f = f i
          def MulEquiv.piSubsingleton {ι : Type u_1} (M : ιType u_2) [inst : (j : ι) → Mul (M j)] [inst : Subsingleton ι] (i : ι) :
          ((j : ι) → M j) ≃* M i

          A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

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

          Groups #

          theorem AddEquiv.map_neg {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] (h : G ≃+ H) (x : G) :
          h (-x) = -h x

          An additive equivalence of additive groups preserves negation.

          theorem MulEquiv.map_inv {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : DivisionMonoid H] (h : G ≃* H) (x : G) :
          h x⁻¹ = (h x)⁻¹

          A multiplicative equivalence of groups preserves inversion.

          theorem AddEquiv.map_sub {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] (h : G ≃+ H) (x : G) (y : G) :
          h (x - y) = h x - h y

          An additive equivalence of additive groups preserves subtractions.

          theorem MulEquiv.map_div {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : DivisionMonoid H] (h : G ≃* H) (x : G) (y : G) :
          h (x / y) = h x / h y

          A multiplicative equivalence of groups preserves division.

          def AddHom.toAddEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :
          M ≃+ N

          Given a pair of additive homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive homomorphisms.

          Equations
          • One or more equations did not get rendered due to their size.
          def AddHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₂ : AddHom.comp f g = AddHom.id N) (x : N) :
          ↑(AddHom.comp f g) x = ↑(AddHom.id N) x
          Equations
          def AddHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (x : M) :
          ↑(AddHom.comp g f) x = ↑(AddHom.id M) x
          Equations
          def MulHom.toMulEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :
          M ≃* N

          Given a pair of multiplicative homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for multiplicative homomorphisms.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem AddHom.toAddEquiv_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :
          ↑(AddHom.toAddEquiv f g h₁ h₂) = f
          @[simp]
          theorem MulHom.toMulEquiv_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :
          ↑(MulHom.toMulEquiv f g h₁ h₂) = f
          @[simp]
          theorem AddHom.toAddEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) :
          ↑(AddEquiv.symm (AddHom.toAddEquiv f g h₁ h₂)) = g
          @[simp]
          theorem MulHom.toMulEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) :
          ↑(MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂)) = g
          def AddMonoidHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (x : M) :
          ↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x
          Equations
          def AddMonoidHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) (x : N) :
          ↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x
          Equations
          def AddMonoidHom.toAddEquiv {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :
          M ≃+ N

          Given a pair of additive monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :
          ↑(MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂)) = g
          @[simp]
          theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :
          ↑(AddEquiv.symm (AddMonoidHom.toAddEquiv f g h₁ h₂)) = g
          @[simp]
          theorem AddMonoidHom.toAddEquiv_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) :
          ↑(AddMonoidHom.toAddEquiv f g h₁ h₂) = f
          @[simp]
          theorem MonoidHom.toMulEquiv_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :
          ↑(MonoidHom.toMulEquiv f g h₁ h₂) = f
          def MonoidHom.toMulEquiv {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) :
          M ≃* N

          Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.

          Equations
          • One or more equations did not get rendered due to their size.
          def Equiv.neg (G : Type u_1) [inst : InvolutiveNeg G] :

          Negation on an AddGroup is a permutation of the underlying type.

          Equations
          @[simp]
          theorem Equiv.neg_apply (G : Type u_1) [inst : InvolutiveNeg G] :
          ↑(Equiv.neg G) = Neg.neg
          @[simp]
          theorem Equiv.inv_apply (G : Type u_1) [inst : InvolutiveInv G] :
          ↑(Equiv.inv G) = Inv.inv
          def Equiv.inv (G : Type u_1) [inst : InvolutiveInv G] :

          Inversion on a Group or GroupWithZero is a permutation of the underlying type.

          Equations
          @[simp]
          theorem Equiv.neg_symm {G : Type u_1} [inst : InvolutiveNeg G] :
          @[simp]
          theorem Equiv.inv_symm {G : Type u_1} [inst : InvolutiveInv G] :