Documentation

Mathlib.Algebra.Group.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

source
@[simp]
theorem EmbeddingLike.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x = 1 ↔ x = 1
source
@[simp]
theorem EmbeddingLike.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x = 0 ↔ x = 0
source
theorem EmbeddingLike.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x ≠ 1 ↔ x ≠ 1
source
theorem EmbeddingLike.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x ≠ 0 ↔ x ≠ 0
source
structure AddEquiv (A : Type u_9) (B : Type u_10) [Add A] [Add B] extends A ≃ B, A →ₙ+ B :
Type (max u_10 u_9)

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

Instances For
source
class AddEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [Add A] [Add B] [EquivLike F A B] :
Prop

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

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

    Preserves addition.

Instances
    source
    structure MulEquiv (M : Type u_9) (N : Type u_10) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N :
    Type (max u_10 u_9)

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

    Instances For
    source
    def «term_≃*_» :
    Lean.TrailingParserDescr

    Notation for a MulEquiv.

    Equations
    source
    def «term_≃+_» :
    Lean.TrailingParserDescr

    Notation for an AddEquiv.

    Equations
    source
    theorem MulEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] :
    Function.Injective MulEquiv.toEquiv
    source
    theorem AddEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Add α] [Add β] :
    Function.Injective AddEquiv.toEquiv
    source
    class MulEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [Mul A] [Mul B] [EquivLike F A B] :
    Prop

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

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

      Preserves multiplication.

    Instances
      source
      @[deprecated EmbeddingLike.map_eq_one_iff]
      theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
      f x = 1 ↔ x = 1

      Alias of EmbeddingLike.map_eq_one_iff.

      source
      @[deprecated EmbeddingLike.map_eq_zero_iff]
      theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
      f x = 0 ↔ x = 0
      source
      @[deprecated EmbeddingLike.map_ne_one_iff]
      theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
      f x ≠ 1 ↔ x ≠ 1

      Alias of EmbeddingLike.map_ne_one_iff.

      source
      @[deprecated EmbeddingLike.map_ne_zero_iff]
      theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
      f x ≠ 0 ↔ x ≠ 0
      source
      theorem MulEquivClass.instMulHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] :
      MulHomClass F M N
      source
      theorem AddEquivClass.instAddHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] :
      AddHomClass F M N
      source
      theorem MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
      MonoidHomClass F M N
      source
      theorem AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [AddZeroClass M] [AddZeroClass N] [AddEquivClass F M N] :
      AddMonoidHomClass F M N
      source
      def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [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
      • ↑f = { toEquiv := ↑f, map_mul' := ⋯ }
      source
      def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [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
      • ↑f = { toEquiv := ↑f, map_add' := ⋯ }
      source
      instance instCoeTCMulEquivOfMulEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
      CoeTC F (α ≃* β)

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

      Equations
      • instCoeTCMulEquivOfMulEquivClass = { coe := MulEquivClass.toMulEquiv }
      source
      instance instCoeTCAddEquivOfAddEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
      CoeTC F (α ≃+ β)

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

      Equations
      • instCoeTCAddEquivOfAddEquivClass = { coe := AddEquivClass.toAddEquiv }
      source
      theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
      Function.Injective MulEquivClass.toMulEquiv
      source
      theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
      Function.Injective AddEquivClass.toAddEquiv
      source
      instance MulEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
      EquivLike (M ≃* N) M N
      Equations
      • MulEquiv.instEquivLike = { coe := fun (f : M ≃* N) => f.toFun, inv := fun (f : M ≃* N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
      source
      instance AddEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
      EquivLike (M ≃+ N) M N
      Equations
      • AddEquiv.instEquivLike = { coe := fun (f : M ≃+ N) => f.toFun, inv := fun (f : M ≃+ N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
      source
      instance MulEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
      CoeFun (M ≃* N) fun (x : M ≃* N) => M → N
      Equations
      • MulEquiv.instCoeFunForall = { coe := fun (f : M ≃* N) => ⇑f }
      source
      instance AddEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
      CoeFun (M ≃+ N) fun (x : M ≃+ N) => M → N
      Equations
      • AddEquiv.instCoeFunForall = { coe := fun (f : M ≃+ N) => ⇑f }
      source
      theorem MulEquiv.instMulEquivClass {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
      MulEquivClass (M ≃* N) M N
      source
      theorem AddEquiv.instAddEquivClass {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
      AddEquivClass (M ≃+ N) M N
      source
      theorem AddEquiv.ext {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f 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.

      source
      theorem MulEquiv.ext {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f 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.

      source
      theorem MulEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} {x x' : M} :
      x = x' → f x = f x'
      source
      theorem AddEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} {x x' : M} :
      x = x' → f x = f x'
      source
      theorem MulEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : f = g) (x : M) :
      f x = g x
      source
      theorem AddEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : f = g) (x : M) :
      f x = g x
      source
      @[simp]
      theorem MulEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
      ⇑{ toEquiv := f, map_mul' := hf } = ⇑f
      source
      @[simp]
      theorem AddEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
      ⇑{ toEquiv := f, map_add' := hf } = ⇑f
      source
      @[simp]
      theorem MulEquiv.mk_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (e' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e
      source
      @[simp]
      theorem AddEquiv.mk_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (e' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e
      source
      @[simp]
      theorem MulEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      f.toEquiv = ↑f
      source
      @[simp]
      theorem AddEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      f.toEquiv = ↑f
      source
      @[simp]
      theorem MulEquiv.toMulHom_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      f.toMulHom = ↑f
      source
      @[simp]
      theorem AddEquiv.toAddHom_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      f.toAddHom = ↑f
      source
      @[simp]
      theorem MulEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      ⇑↑f = ⇑f
      source
      @[simp]
      theorem AddEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      ⇑↑f = ⇑f
      source
      @[simp]
      theorem MulEquiv.coe_toMulHom {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
      ⇑f.toMulHom = ⇑f
      source
      @[simp]
      theorem AddEquiv.coe_toAddHom {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
      ⇑f.toAddHom = ⇑f
      source
      def MulEquiv.mk' {M : Type u_4} {N : Type u_5} [Mul M] [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
      source
      def AddEquiv.mk' {M : Type u_4} {N : Type u_5} [Add M] [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
      source
      @[deprecated map_mul]
      theorem MulEquiv.map_mul {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) (x y : M) :
      f (x * y) = f x * f y

      A multiplicative isomorphism preserves multiplication.

      source
      @[deprecated map_add]
      theorem AddEquiv.map_add {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (x y : M) :
      f (x + y) = f x + f y

      An additive isomorphism preserves addition.

      source
      theorem MulEquiv.bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      Function.Bijective ⇑e
      source
      theorem AddEquiv.bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      Function.Bijective ⇑e
      source
      theorem MulEquiv.injective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      Function.Injective ⇑e
      source
      theorem AddEquiv.injective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      Function.Injective ⇑e
      source
      theorem MulEquiv.surjective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      Function.Surjective ⇑e
      source
      theorem AddEquiv.surjective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      Function.Surjective ⇑e
      source
      theorem MulEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x y : M} :
      e x = e y ↔ x = y
      source
      theorem AddEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x y : M} :
      e x = e y ↔ x = y
      source
      def MulEquiv.refl (M : Type u_9) [Mul M] :
      M ≃* M

      The identity map is a multiplicative isomorphism.

      Equations
      source
      def AddEquiv.refl (M : Type u_9) [Add M] :
      M ≃+ M

      The identity map is an additive isomorphism.

      Equations
      source
      instance MulEquiv.instInhabited {M : Type u_4} [Mul M] :
      Inhabited (M ≃* M)
      Equations
      source
      instance AddEquiv.instInhabited {M : Type u_4} [Add M] :
      Inhabited (M ≃+ M)
      Equations
      source
      @[simp]
      theorem MulEquiv.coe_refl {M : Type u_4} [Mul M] :
      ⇑(MulEquiv.refl M) = id
      source
      @[simp]
      theorem AddEquiv.coe_refl {M : Type u_4} [Add M] :
      ⇑(AddEquiv.refl M) = id
      source
      @[simp]
      theorem MulEquiv.refl_apply {M : Type u_4} [Mul M] (m : M) :
      (MulEquiv.refl M) m = m
      source
      @[simp]
      theorem AddEquiv.refl_apply {M : Type u_4} [Add M] (m : M) :
      (AddEquiv.refl M) m = m
      source
      theorem MulEquiv.symm_map_mul {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) (x y : N) :
      h.symm (x * y) = h.symm x * h.symm y

      An alias for h.symm.map_mul. Introduced to fix the issue in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth

      source
      theorem AddEquiv.symm_map_add {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) (x y : N) :
      h.symm (x + y) = h.symm x + h.symm y
      source
      def MulEquiv.symm {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) :
      N ≃* M

      The inverse of an isomorphism is an isomorphism.

      Equations
      • h.symm = { toEquiv := h.symm, map_mul' := ⋯ }
      source
      def AddEquiv.symm {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) :
      N ≃+ M

      The inverse of an isomorphism is an isomorphism.

      Equations
      • h.symm = { toEquiv := h.symm, map_add' := ⋯ }
      source
      theorem MulEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
      f.invFun = ⇑f.symm
      source
      theorem AddEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
      f.invFun = ⇑f.symm
      source
      @[simp]
      theorem MulEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      ⇑(↑f).symm = ⇑f.symm
      source
      @[simp]
      theorem AddEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      ⇑(↑f).symm = ⇑f.symm
      source
      @[simp]
      theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      EquivLike.inv f = ⇑f.symm
      source
      @[simp]
      theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      EquivLike.inv f = ⇑f.symm
      source
      @[simp]
      theorem MulEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      ↑f.symm = (↑f).symm
      source
      @[simp]
      theorem AddEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      ↑f.symm = (↑f).symm
      source
      @[simp]
      theorem MulEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
      f.symm.symm = f
      source
      @[simp]
      theorem AddEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
      f.symm.symm = f
      source
      theorem MulEquiv.symm_bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
      Function.Bijective MulEquiv.symm
      source
      theorem AddEquiv.symm_bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
      Function.Bijective AddEquiv.symm
      source
      @[simp]
      theorem MulEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (f : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) :
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm
      source
      @[simp]
      theorem AddEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (f : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) :
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm
      source
      @[simp]
      theorem MulEquiv.symm_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) :
      { toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := ⋯ }
      source
      @[simp]
      theorem AddEquiv.symm_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y) :
      { toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := ⋯ }
      source
      @[simp]
      theorem MulEquiv.refl_symm {M : Type u_4} [Mul M] :
      (MulEquiv.refl M).symm = MulEquiv.refl M
      source
      @[simp]
      theorem AddEquiv.refl_symm {M : Type u_4} [Add M] :
      (AddEquiv.refl M).symm = AddEquiv.refl M
      source
      @[simp]
      theorem MulEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (y : N) :
      e (e.symm y) = y

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

      source
      @[simp]
      theorem AddEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (y : N) :
      e (e.symm y) = y

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

      source
      @[simp]
      theorem MulEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (x : M) :
      e.symm (e x) = x

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

      source
      @[simp]
      theorem AddEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (x : M) :
      e.symm (e x) = x

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

      source
      @[simp]
      theorem MulEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      ⇑e.symm ∘ ⇑e = id
      source
      @[simp]
      theorem AddEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      ⇑e.symm ∘ ⇑e = id
      source
      @[simp]
      theorem MulEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      ⇑e ∘ ⇑e.symm = id
      source
      @[simp]
      theorem AddEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      ⇑e ∘ ⇑e.symm = id
      source
      theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} :
      e x = y ↔ x = e.symm y
      source
      theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} :
      e x = y ↔ x = e.symm y
      source
      theorem MulEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
      e.symm x = y ↔ x = e y
      source
      theorem AddEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
      e.symm x = y ↔ x = e y
      source
      theorem MulEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
      y = e.symm x ↔ e y = x
      source
      theorem AddEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
      y = e.symm x ↔ e y = x
      source
      theorem MulEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) :
      f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
      source
      theorem AddEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) :
      f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
      source
      theorem MulEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) :
      g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
      source
      theorem AddEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) :
      g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
      source
      theorem MulEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) :
      f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
      source
      theorem AddEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) :
      f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
      source
      theorem MulEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) :
      ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
      source
      theorem AddEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) :
      ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
      source
      @[simp]
      theorem MulEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) :
      e ((↑e).symm x) = x
      source
      @[simp]
      theorem AddEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : β) :
      e ((↑e).symm x) = x
      source
      @[simp]
      theorem MulEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) :
      (↑e).symm (e x) = x
      source
      @[simp]
      theorem AddEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : α) :
      (↑e).symm (e x) = x
      source
      def MulEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      N → M

      See Note [custom simps projection]

      Equations
      source
      def AddEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      N → M

      See Note [custom simps projection]

      Equations
      source
      def MulEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
      M ≃* P

      Transitivity of multiplication-preserving isomorphisms

      Equations
      • h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_mul' := ⋯ }
      source
      def AddEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
      M ≃+ P

      Transitivity of addition-preserving isomorphisms

      Equations
      • h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_add' := ⋯ }
      source
      @[simp]
      theorem MulEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
      ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
      source
      @[simp]
      theorem AddEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
      ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
      source
      @[simp]
      theorem MulEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
      (e₁.trans e₂) m = e₂ (e₁ m)
      source
      @[simp]
      theorem AddEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
      (e₁.trans e₂) m = e₂ (e₁ m)
      source
      @[simp]
      theorem MulEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
      (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
      source
      @[simp]
      theorem AddEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
      (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
      source
      @[simp]
      theorem MulEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      e.symm.trans e = MulEquiv.refl N
      source
      @[simp]
      theorem AddEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      e.symm.trans e = AddEquiv.refl N
      source
      @[simp]
      theorem MulEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
      e.trans e.symm = MulEquiv.refl M
      source
      @[simp]
      theorem AddEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
      e.trans e.symm = AddEquiv.refl M
      source
      def MulEquiv.mulEquivOfUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Mul M] [Mul N] :
      M ≃* N

      The MulEquiv between two monoids with a unique element.

      Equations
      source
      def AddEquiv.addEquivOfUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Add M] [Add N] :
      M ≃+ N

      The AddEquiv between two AddMonoids with a unique element.

      Equations
      source
      instance MulEquiv.instUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Mul M] [Mul N] :
      Unique (M ≃* N)

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

      Equations
      • MulEquiv.instUnique = { default := MulEquiv.mulEquivOfUnique, uniq := ⋯ }
      source
      instance AddEquiv.instUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Add M] [Add N] :
      Unique (M ≃+ N)

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

      Equations
      • AddEquiv.instUnique = { default := AddEquiv.addEquivOfUnique, uniq := ⋯ }

      Monoids #

      source
      theorem MulEquiv.coe_monoidHom_refl {M : Type u_4} [MulOneClass M] :
      ↑(MulEquiv.refl M) = MonoidHom.id M
      source
      theorem AddEquiv.coe_addMonoidHom_refl {M : Type u_4} [AddZeroClass M] :
      ↑(AddEquiv.refl M) = AddMonoidHom.id M
      source
      theorem MulEquiv.coe_monoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
      ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
      source
      theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
      ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
      source
      @[simp]
      theorem MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
      (↑e).comp ↑e.symm = MonoidHom.id N
      source
      @[simp]
      theorem AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
      (↑e).comp ↑e.symm = AddMonoidHom.id N
      source
      @[simp]
      theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
      (↑e.symm).comp ↑e = MonoidHom.id M
      source
      @[simp]
      theorem AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
      (↑e.symm).comp ↑e = AddMonoidHom.id M
      source
      theorem MulEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
      Function.Injective fun (f : N →* P) => f.comp ↑e
      source
      theorem AddEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
      Function.Injective fun (f : N →+ P) => f.comp ↑e
      source
      theorem MulEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
      Function.Injective fun (f : P →* M) => (↑e).comp f
      source
      theorem AddEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
      Function.Injective fun (f : P →+ M) => (↑e).comp f
      source
      theorem MulEquiv.map_one {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
      h 1 = 1

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

      source
      theorem AddEquiv.map_zero {M : Type u_4} {N : Type u_5} [AddZeroClass M] [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).

      source
      theorem MulEquiv.map_eq_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
      h x = 1 ↔ x = 1
      source
      theorem AddEquiv.map_eq_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
      h x = 0 ↔ x = 0
      source
      theorem MulEquiv.map_ne_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
      h x ≠ 1 ↔ x ≠ 1
      source
      theorem AddEquiv.map_ne_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
      h x ≠ 0 ↔ x ≠ 0
      source
      noncomputable def MulEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) :
      M ≃* N

      A bijective Semigroup homomorphism is an isomorphism

      Equations
      source
      noncomputable def AddEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) :
      M ≃+ N

      A bijective AddSemigroup homomorphism is an isomorphism

      Equations
      source
      @[simp]
      theorem AddEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) :
      (AddEquiv.ofBijective f hf) a = f a
      source
      @[simp]
      theorem MulEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) :
      (MulEquiv.ofBijective f hf) a = f a
      source
      @[simp]
      theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective ⇑f) :
      f ((MulEquiv.ofBijective f hf).symm n) = n
      source
      @[simp]
      theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective ⇑f) :
      f ((AddEquiv.ofBijective f hf).symm n) = n
      source
      def MulEquiv.toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
      M →* N

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

      Equations
      • h.toMonoidHom = { toFun := h.toFun, map_one' := ⋯, map_mul' := ⋯ }
      source
      def AddEquiv.toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :
      M →+ N

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

      Equations
      • h.toAddMonoidHom = { toFun := h.toFun, map_zero' := ⋯, map_add' := ⋯ }
      source
      @[simp]
      theorem MulEquiv.coe_toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
      ⇑e.toMonoidHom = ⇑e
      source
      @[simp]
      theorem AddEquiv.coe_toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
      ⇑e.toAddMonoidHom = ⇑e
      source
      @[simp]
      theorem MulEquiv.toMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M ≃* N) :
      f.toMonoidHom = ↑f
      source
      @[simp]
      theorem AddEquiv.toAddMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) :
      f.toAddMonoidHom = ↑f
      source
      theorem MulEquiv.toMonoidHom_injective {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
      Function.Injective MulEquiv.toMonoidHom
      source
      theorem AddEquiv.toAddMonoidHom_injective {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
      Function.Injective AddEquiv.toAddMonoidHom
      source
      def MulEquiv.arrowCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) :
      (M → P) ≃* (N → Q)

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

      Equations
      • MulEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
      source
      def AddEquiv.arrowCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Add P] [Add Q] (f : M ≃ N) (g : P ≃+ Q) :
      (M → P) ≃+ (N → Q)

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

      Equations
      • AddEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
      source
      @[simp]
      theorem AddEquiv.arrowCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Add P] [Add Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) (n : N) :
      (AddEquiv.arrowCongr f g) h n = g (h (f.symm n))
      source
      @[simp]
      theorem MulEquiv.arrowCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) (h : M → P) (n : N) :
      (MulEquiv.arrowCongr f g) h n = g (h (f.symm n))
      source
      def MulEquiv.monoidHomCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [MulOneClass M] [MulOneClass N] [CommMonoid P] [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.
      source
      def AddEquiv.addMonoidHomCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [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.
      source
      @[simp]
      theorem MulEquiv.monoidHomCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
      (f.monoidHomCongr g) h = g.toMonoidHom.comp (h.comp f.symm.toMonoidHom)
      source
      @[simp]
      theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
      (f.addMonoidHomCongr g) h = g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)
      source
      def MulEquiv.piCongrRight {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Mul (Ms j)] [(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) 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.
      source
      def AddEquiv.piCongrRight {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Add (Ms j)] [(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) 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.
      source
      @[simp]
      theorem AddEquiv.piCongrRight_apply {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
      (AddEquiv.piCongrRight es) x j = (es j) (x j)
      source
      @[simp]
      theorem MulEquiv.piCongrRight_apply {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
      (MulEquiv.piCongrRight es) x j = (es j) (x j)
      source
      @[simp]
      theorem MulEquiv.piCongrRight_refl {η : Type u_9} {Ms : η → Type u_10} [(j : η) → Mul (Ms j)] :
      (MulEquiv.piCongrRight fun (j : η) => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
      source
      @[simp]
      theorem AddEquiv.piCongrRight_refl {η : Type u_9} {Ms : η → Type u_10} [(j : η) → Add (Ms j)] :
      (AddEquiv.piCongrRight fun (j : η) => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
      source
      @[simp]
      theorem MulEquiv.piCongrRight_symm {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
      (MulEquiv.piCongrRight es).symm = MulEquiv.piCongrRight fun (i : η) => (es i).symm
      source
      @[simp]
      theorem AddEquiv.piCongrRight_symm {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
      (AddEquiv.piCongrRight es).symm = AddEquiv.piCongrRight fun (i : η) => (es i).symm
      source
      @[simp]
      theorem MulEquiv.piCongrRight_trans {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} {Ps : η → Type u_12} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
      (MulEquiv.piCongrRight es).trans (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun (i : η) => (es i).trans (fs i)
      source
      @[simp]
      theorem AddEquiv.piCongrRight_trans {η : Type u_9} {Ms : η → Type u_10} {Ns : η → Type u_11} {Ps : η → Type u_12} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
      (AddEquiv.piCongrRight es).trans (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun (i : η) => (es i).trans (fs i)
      source
      def MulEquiv.piUnique {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Mul (M j)] [Unique ι] :
      ((j : ι) → M j) ≃* M default

      A family indexed by a type with a unique element is MulEquiv to the element at the single index.

      Equations
      source
      def AddEquiv.piUnique {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Add (M j)] [Unique ι] :
      ((j : ι) → M j) ≃+ M default

      A family indexed by a type with a unique element is AddEquiv to the element at the single index.

      Equations
      source
      @[simp]
      theorem MulEquiv.piUnique_symm_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) :
      (MulEquiv.piUnique M).symm x i = uniqueElim x i
      source
      @[simp]
      theorem MulEquiv.piUnique_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) :
      (MulEquiv.piUnique M) f = f default
      source
      @[simp]
      theorem AddEquiv.piUnique_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) :
      (AddEquiv.piUnique M) f = f default
      source
      @[simp]
      theorem AddEquiv.piUnique_symm_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) :
      (AddEquiv.piUnique M).symm x i = uniqueElim x i

      Groups #

      source
      theorem MulEquiv.map_inv {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :
      h x⁻¹ = (h x)⁻¹

      A multiplicative equivalence of groups preserves inversion.

      source
      theorem AddEquiv.map_neg {G : Type u_7} {H : Type u_8} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x : G) :
      h (-x) = -h x

      An additive equivalence of additive groups preserves negation.

      source
      theorem MulEquiv.map_div {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) :
      h (x / y) = h x / h y

      A multiplicative equivalence of groups preserves division.

      source
      theorem AddEquiv.map_sub {G : Type u_7} {H : Type u_8} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x y : G) :
      h (x - y) = h x - h y

      An additive equivalence of additive groups preserves subtractions.

      source
      def MulHom.toMulEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp 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 a 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
      • f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
      source
      def AddHom.toAddEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp 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
      • f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
      source
      @[simp]
      theorem MulHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N) :
      ⇑(f.toMulEquiv g h₁ h₂) = ⇑f
      source
      @[simp]
      theorem AddHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N) :
      ⇑(f.toAddEquiv g h₁ h₂) = ⇑f
      source
      @[simp]
      theorem MulHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N) :
      ⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
      source
      @[simp]
      theorem AddHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = AddHom.id M) (h₂ : f.comp g = AddHom.id N) :
      ⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
      source
      def MonoidHom.toMulEquiv {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp 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 a 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
      • f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
      source
      def AddMonoidHom.toAddEquiv {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp 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
      • f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
      source
      @[simp]
      theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N) :
      ⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
      source
      @[simp]
      theorem AddMonoidHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N) :
      ⇑(f.toAddEquiv g h₁ h₂) = ⇑f
      source
      @[simp]
      theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N) :
      ⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
      source
      @[simp]
      theorem MonoidHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N) :
      ⇑(f.toMulEquiv g h₁ h₂) = ⇑f
      source
      def Equiv.inv (G : Type u_7) [InvolutiveInv G] :
      Equiv.Perm G

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

      Equations
      source
      def Equiv.neg (G : Type u_7) [InvolutiveNeg G] :
      Equiv.Perm G

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

      Equations
      source
      @[simp]
      theorem Equiv.inv_apply (G : Type u_7) [InvolutiveInv G] :
      ⇑(Equiv.inv G) = Inv.inv
      source
      @[simp]
      theorem Equiv.neg_apply (G : Type u_7) [InvolutiveNeg G] :
      ⇑(Equiv.neg G) = Neg.neg
      source
      @[simp]
      theorem Equiv.inv_symm {G : Type u_7} [InvolutiveInv G] :
      Equiv.symm (Equiv.inv G) = Equiv.inv G
      source
      @[simp]
      theorem Equiv.neg_symm {G : Type u_7} [InvolutiveNeg G] :
      Equiv.symm (Equiv.neg G) = Equiv.neg G