Documentation

Mathlib.Topology.Algebra.ContinuousMonoidHom

Continuous Monoid Homs #

This file defines the space of continuous homomorphisms between two topological groups.

Main definitions #

structure ContinuousAddMonoidHom (A : Type u_7) (B : Type u_8) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends A →+ B, C(A, B) :
Type (max u_7 u_8)

The type of continuous additive monoid homomorphisms from A to B.

Instances For
    structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends A →* B, C(A, B) :
    Type (max u_2 u_3)

    The type of continuous monoid homomorphisms from A to B.

    When possible, instead of parametrizing results over (f : ContinuousMonoidHom A B), you should parametrize over (F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F).

    When you extend this structure, make sure to extend ContinuousMapClass and/or MonoidHomClass, if needed.

    Instances For

      The type of continuous monoid homomorphisms from A to B.

      Equations
        Instances For

          The type of continuous monoid homomorphisms from A to B.

          Equations
            Instances For
              Equations
                @[simp]
                theorem ContinuousMonoidHom.coe_toMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) :
                f.toMonoidHom = f
                def ContinuousMonoidHom.toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :

                Turn an element of a type F satisfying MonoidHomClass F A B and ContinuousMapClass F A B into aContinuousMonoidHom. This is declared as the default coercion from F to (A →ₜ* B).

                Equations
                  Instances For

                    Turn an element of a type F satisfying AddMonoidHomClass F A B and ContinuousMapClass F A B into aContinuousAddMonoidHom. This is declared as the default coercion from F to ContinuousAddMonoidHom A B.

                    Equations
                      Instances For
                        @[simp]
                        theorem ContinuousMonoidHom.coe_coe {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
                        f = f
                        @[simp]
                        theorem ContinuousAddMonoidHom.coe_coe {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
                        f = f
                        @[simp]
                        theorem ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
                        f = f
                        @[simp]
                        @[simp]
                        theorem ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) :
                        f = f
                        @[simp]
                        theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ* B} (h : ∀ (x : A), f x = g x) :
                        f = g
                        theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ+ B} (h : ∀ (x : A), f x = g x) :
                        f = g
                        theorem ContinuousAddMonoidHom.ext_iff {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ+ B} :
                        f = g ∀ (x : A), f x = g x
                        theorem ContinuousMonoidHom.ext_iff {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ* B} :
                        f = g ∀ (x : A), f x = g x
                        def ContinuousMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B) :

                        Composition of two continuous homomorphisms.

                        Equations
                          Instances For
                            def ContinuousAddMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B) :

                            Composition of two continuous homomorphisms.

                            Equations
                              Instances For
                                @[simp]
                                theorem ContinuousMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B) (a✝ : A) :
                                (g.comp f) a✝ = g (f a✝)
                                @[simp]
                                theorem ContinuousAddMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B) (a✝ : A) :
                                (g.comp f) a✝ = g (f a✝)
                                @[simp]
                                theorem ContinuousMonoidHom.coe_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B) :
                                (g.comp f) = g f
                                @[simp]
                                theorem ContinuousAddMonoidHom.coe_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ+ C) (f : A →ₜ+ B) :
                                (g.comp f) = g f
                                def ContinuousMonoidHom.prod {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : A →ₜ* B) (g : A →ₜ* C) :
                                A →ₜ* B × C

                                Product of two continuous homomorphisms on the same space.

                                Equations
                                  Instances For
                                    def ContinuousAddMonoidHom.prod {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : A →ₜ+ B) (g : A →ₜ+ C) :
                                    A →ₜ+ B × C

                                    Product of two continuous homomorphisms on the same space.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem ContinuousAddMonoidHom.prod_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : A →ₜ+ B) (g : A →ₜ+ C) (i : A) :
                                        (f.prod g) i = (f i, g i)
                                        @[simp]
                                        theorem ContinuousMonoidHom.prod_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : A →ₜ* B) (g : A →ₜ* C) (i : A) :
                                        (f.prod g) i = (f i, g i)
                                        def ContinuousMonoidHom.prodMap {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Monoid B] [Monoid C] [Monoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A →ₜ* C) (g : B →ₜ* D) :
                                        A × B →ₜ* C × D

                                        Product of two continuous homomorphisms on different spaces.

                                        Equations
                                          Instances For
                                            def ContinuousAddMonoidHom.prodMap {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A →ₜ+ C) (g : B →ₜ+ D) :
                                            A × B →ₜ+ C × D

                                            Product of two continuous homomorphisms on different spaces.

                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem ContinuousMonoidHom.prodMap_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Monoid B] [Monoid C] [Monoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A →ₜ* C) (g : B →ₜ* D) (i : A × B) :
                                                (f.prodMap g) i = (f i.1, g i.2)
                                                @[simp]
                                                theorem ContinuousAddMonoidHom.prodMap_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A →ₜ+ C) (g : B →ₜ+ D) (i : A × B) :
                                                (f.prodMap g) i = (f i.1, g i.2)
                                                instance ContinuousMonoidHom.instOne (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                One (A →ₜ* B)

                                                The trivial continuous homomorphism.

                                                Equations

                                                  The trivial continuous homomorphism.

                                                  Equations
                                                    @[simp]
                                                    theorem ContinuousAddMonoidHom.zero_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (x✝ : A) :
                                                    0 x✝ = 0
                                                    @[simp]
                                                    theorem ContinuousMonoidHom.one_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (x✝ : A) :
                                                    1 x✝ = 1
                                                    @[simp]
                                                    theorem ContinuousMonoidHom.coe_one (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                    1 = 1
                                                    @[simp]

                                                    The identity continuous homomorphism.

                                                    Equations
                                                      Instances For

                                                        The identity continuous homomorphism.

                                                        Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem ContinuousAddMonoidHom.id_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (x : A) :
                                                            (id A) x = x
                                                            @[simp]
                                                            theorem ContinuousMonoidHom.id_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (x : A) :
                                                            (id A) x = x
                                                            @[simp]

                                                            The continuous homomorphism given by projection onto the first factor.

                                                            Equations
                                                              Instances For

                                                                The continuous homomorphism given by projection onto the first factor.

                                                                Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                                                    (fst A B) self = self.1
                                                                    @[simp]
                                                                    theorem ContinuousAddMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                                                    (fst A B) self = self.1

                                                                    The continuous homomorphism given by projection onto the second factor.

                                                                    Equations
                                                                      Instances For

                                                                        The continuous homomorphism given by projection onto the second factor.

                                                                        Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem ContinuousAddMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                                                            (snd A B) self = self.2
                                                                            @[simp]
                                                                            theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                                                            (snd A B) self = self.2

                                                                            The continuous homomorphism given by inclusion of the first factor.

                                                                            Equations
                                                                              Instances For

                                                                                The continuous homomorphism given by inclusion of the first factor.

                                                                                Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem ContinuousMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                                                                    (inl A B) i = (i, 1)
                                                                                    @[simp]
                                                                                    theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                                                                    (inl A B) i = (i, 0)

                                                                                    The continuous homomorphism given by inclusion of the second factor.

                                                                                    Equations
                                                                                      Instances For

                                                                                        The continuous homomorphism given by inclusion of the second factor.

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem ContinuousMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                                                                            (inr A B) i = (1, i)
                                                                                            @[simp]
                                                                                            theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                                                                            (inr A B) i = (0, i)

                                                                                            The continuous homomorphism given by the diagonal embedding.

                                                                                            Equations
                                                                                              Instances For

                                                                                                The continuous homomorphism given by the diagonal embedding.

                                                                                                Equations
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem ContinuousAddMonoidHom.diag_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (i : A) :
                                                                                                    (diag A) i = (i, i)
                                                                                                    @[simp]
                                                                                                    theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (i : A) :
                                                                                                    (diag A) i = (i, i)
                                                                                                    def ContinuousMonoidHom.swap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                                                    A × B →ₜ* B × A

                                                                                                    The continuous homomorphism given by swapping components.

                                                                                                    Equations
                                                                                                      Instances For

                                                                                                        The continuous homomorphism given by swapping components.

                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            @[simp]
                                                                                                            theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                                                                            (swap A B) i = (i.2, i.1)
                                                                                                            @[simp]
                                                                                                            theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                                                                            (swap A B) i = (i.2, i.1)

                                                                                                            The continuous homomorphism given by multiplication.

                                                                                                            Equations
                                                                                                              Instances For

                                                                                                                The continuous homomorphism given by addition.

                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    @[simp]
                                                                                                                    theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (a✝ : E × E) :
                                                                                                                    (mul E) a✝ = a✝.1 * a✝.2
                                                                                                                    @[simp]
                                                                                                                    theorem ContinuousAddMonoidHom.add_toFun (E : Type u_6) [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (a✝ : E × E) :
                                                                                                                    (add E) a✝ = a✝.1 + a✝.2
                                                                                                                    def ContinuousMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f : A →ₜ* E) (g : B →ₜ* E) :
                                                                                                                    A × B →ₜ* E

                                                                                                                    Coproduct of two continuous homomorphisms to the same space.

                                                                                                                    Equations
                                                                                                                      Instances For

                                                                                                                        Coproduct of two continuous homomorphisms to the same space.

                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            @[simp]
                                                                                                                            theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f : A →ₜ* E) (g : B →ₜ* E) (a✝ : A × B) :
                                                                                                                            (f.coprod g) a✝ = f a✝.1 * g a✝.2
                                                                                                                            @[simp]
                                                                                                                            theorem ContinuousAddMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (f : A →ₜ+ E) (g : B →ₜ+ E) (a✝ : A × B) :
                                                                                                                            (f.coprod g) a✝ = f a✝.1 + g a✝.2

                                                                                                                            The continuous homomorphism given by inversion.

                                                                                                                            Equations
                                                                                                                              Instances For

                                                                                                                                The continuous homomorphism given by negation.

                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    @[simp]
                                                                                                                                    theorem ContinuousMonoidHom.inv_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [IsTopologicalGroup E] (a✝ : E) :
                                                                                                                                    (inv E) a✝ = a✝⁻¹
                                                                                                                                    @[simp]
                                                                                                                                    theorem ContinuousAddMonoidHom.neg_toFun (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] (a✝ : E) :
                                                                                                                                    (neg E) a✝ = -a✝
                                                                                                                                    def ContinuousMonoidHom.ofClass (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (F : Type u_7) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F) :

                                                                                                                                    For f : F where F is a class of continuous monoid hom, this yields an element ContinuousMonoidHom A B.

                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        def ContinuousAddMonoidHom.ofClass (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (F : Type u_7) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F) :

                                                                                                                                        For f : F where F is a class of continuous additive monoid hom, this yields an element ContinuousAddMonoidHom A B.

                                                                                                                                        Equations
                                                                                                                                          Instances For

                                                                                                                                            Continuous MulEquiv #

                                                                                                                                            This section defines the space of continuous isomorphisms between two topological groups.

                                                                                                                                            Main definitions #

                                                                                                                                            structure ContinuousAddEquiv (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] extends G ≃+ H, G ≃ₜ H :
                                                                                                                                            Type (max u v)

                                                                                                                                            The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.

                                                                                                                                            Instances For
                                                                                                                                              structure ContinuousMulEquiv (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Mul G] [Mul H] extends G ≃* H, G ≃ₜ H :
                                                                                                                                              Type (max u v)

                                                                                                                                              The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.

                                                                                                                                              Instances For

                                                                                                                                                The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.

                                                                                                                                                Equations
                                                                                                                                                  Instances For

                                                                                                                                                    The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.

                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        instance ContinuousMulEquiv.instEquivLike {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] :
                                                                                                                                                        EquivLike (M ≃ₜ* N) M N
                                                                                                                                                        Equations
                                                                                                                                                          instance ContinuousAddEquiv.instEquivLike {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] :
                                                                                                                                                          EquivLike (M ≃ₜ+ N) M N
                                                                                                                                                          Equations
                                                                                                                                                            theorem ContinuousMulEquiv.ext {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {f g : M ≃ₜ* N} (h : ∀ (x : M), f x = g x) :
                                                                                                                                                            f = g

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

                                                                                                                                                            theorem ContinuousAddEquiv.ext {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f g : M ≃ₜ+ N} (h : ∀ (x : M), f x = g x) :
                                                                                                                                                            f = g

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

                                                                                                                                                            theorem ContinuousMulEquiv.ext_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {f g : M ≃ₜ* N} :
                                                                                                                                                            f = g ∀ (x : M), f x = g x
                                                                                                                                                            theorem ContinuousAddEquiv.ext_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f g : M ≃ₜ+ N} :
                                                                                                                                                            f = g ∀ (x : M), f x = g x
                                                                                                                                                            @[simp]
                                                                                                                                                            theorem ContinuousMulEquiv.coe_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃* N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun) :
                                                                                                                                                            { toMulEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = f
                                                                                                                                                            @[simp]
                                                                                                                                                            theorem ContinuousAddEquiv.coe_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃+ N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun) :
                                                                                                                                                            { toAddEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = f
                                                                                                                                                            theorem ContinuousMulEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) :
                                                                                                                                                            f.toEquiv = f
                                                                                                                                                            theorem ContinuousAddEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) :
                                                                                                                                                            f.toEquiv = f
                                                                                                                                                            @[simp]
                                                                                                                                                            theorem ContinuousMulEquiv.toMulEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) :
                                                                                                                                                            f.toMulEquiv = f
                                                                                                                                                            @[simp]
                                                                                                                                                            theorem ContinuousAddEquiv.toAddEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) :
                                                                                                                                                            f.toAddEquiv = f
                                                                                                                                                            def ContinuousMulEquiv.mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y) :

                                                                                                                                                            Makes a continuous multiplicative isomorphism from a homeomorphism which preserves multiplication.

                                                                                                                                                            Equations
                                                                                                                                                              Instances For
                                                                                                                                                                def ContinuousAddEquiv.mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x + y) = f x + f y) :

                                                                                                                                                                Makes an continuous additive isomorphism from a homeomorphism which preserves addition.

                                                                                                                                                                Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[simp]
                                                                                                                                                                    theorem ContinuousMulEquiv.coe_mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y) :
                                                                                                                                                                    (mk' f h) = f
                                                                                                                                                                    theorem ContinuousMulEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x y : M} :
                                                                                                                                                                    e x = e y x = y
                                                                                                                                                                    theorem ContinuousAddEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x y : M} :
                                                                                                                                                                    e x = e y x = y

                                                                                                                                                                    The identity map is a continuous multiplicative isomorphism.

                                                                                                                                                                    Equations
                                                                                                                                                                      Instances For

                                                                                                                                                                        The identity map is a continuous additive isomorphism.

                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem ContinuousMulEquiv.coe_refl (M : Type u_1) [TopologicalSpace M] [Mul M] :
                                                                                                                                                                            (refl M) = id
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem ContinuousAddEquiv.coe_refl (M : Type u_1) [TopologicalSpace M] [Add M] :
                                                                                                                                                                            (refl M) = id
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem ContinuousMulEquiv.refl_apply (M : Type u_1) [TopologicalSpace M] [Mul M] (m : M) :
                                                                                                                                                                            (refl M) m = m
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem ContinuousAddEquiv.refl_apply (M : Type u_1) [TopologicalSpace M] [Add M] (m : M) :
                                                                                                                                                                            (refl M) m = m
                                                                                                                                                                            def ContinuousMulEquiv.symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (cme : M ≃ₜ* N) :

                                                                                                                                                                            The inverse of a ContinuousMulEquiv.

                                                                                                                                                                            Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                def ContinuousAddEquiv.symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (cme : M ≃ₜ+ N) :

                                                                                                                                                                                The inverse of a ContinuousAddEquiv.

                                                                                                                                                                                Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    theorem ContinuousMulEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {f : M ≃ₜ* N} :
                                                                                                                                                                                    f.invFun = f.symm
                                                                                                                                                                                    theorem ContinuousAddEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f : M ≃ₜ+ N} :
                                                                                                                                                                                    f.invFun = f.symm
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.coe_toHomeomorph_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) :
                                                                                                                                                                                    (↑f).symm = f.symm
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.coe_toHomeomorph_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) :
                                                                                                                                                                                    (↑f).symm = f.symm
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.symm_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) :
                                                                                                                                                                                    f.symm.symm = f
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.symm_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) :
                                                                                                                                                                                    f.symm.symm = f
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [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.

                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [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.

                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [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.

                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [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.

                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) :
                                                                                                                                                                                    e.symm e = id
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) :
                                                                                                                                                                                    e.symm e = id
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousMulEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) :
                                                                                                                                                                                    e e.symm = id
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem ContinuousAddEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) :
                                                                                                                                                                                    e e.symm = id
                                                                                                                                                                                    theorem ContinuousMulEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : M} {y : N} :
                                                                                                                                                                                    e x = y x = e.symm y
                                                                                                                                                                                    theorem ContinuousAddEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : M} {y : N} :
                                                                                                                                                                                    e x = y x = e.symm y
                                                                                                                                                                                    theorem ContinuousMulEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : N} {y : M} :
                                                                                                                                                                                    e.symm x = y x = e y
                                                                                                                                                                                    theorem ContinuousAddEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : N} {y : M} :
                                                                                                                                                                                    e.symm x = y x = e y
                                                                                                                                                                                    theorem ContinuousMulEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : N} {y : M} :
                                                                                                                                                                                    y = e.symm x e y = x
                                                                                                                                                                                    theorem ContinuousAddEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : N} {y : M} :
                                                                                                                                                                                    y = e.symm x e y = x
                                                                                                                                                                                    theorem ContinuousMulEquiv.eq_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : Nα) (g : Mα) :
                                                                                                                                                                                    f = g e.symm f e = g
                                                                                                                                                                                    theorem ContinuousAddEquiv.eq_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : Nα) (g : Mα) :
                                                                                                                                                                                    f = g e.symm f e = g
                                                                                                                                                                                    theorem ContinuousMulEquiv.comp_symm_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : Nα) (g : Mα) :
                                                                                                                                                                                    g e.symm = f g = f e
                                                                                                                                                                                    theorem ContinuousAddEquiv.comp_symm_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : Nα) (g : Mα) :
                                                                                                                                                                                    g e.symm = f g = f e
                                                                                                                                                                                    theorem ContinuousMulEquiv.eq_symm_comp {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : αM) (g : αN) :
                                                                                                                                                                                    f = e.symm g e f = g
                                                                                                                                                                                    theorem ContinuousAddEquiv.eq_symm_comp {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : αM) (g : αN) :
                                                                                                                                                                                    f = e.symm g e f = g
                                                                                                                                                                                    theorem ContinuousMulEquiv.symm_comp_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : αM) (g : αN) :
                                                                                                                                                                                    e.symm g = f g = e f
                                                                                                                                                                                    theorem ContinuousAddEquiv.symm_comp_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : αM) (g : αN) :
                                                                                                                                                                                    e.symm g = f g = e f
                                                                                                                                                                                    def ContinuousMulEquiv.trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L) :

                                                                                                                                                                                    The composition of two ContinuousMulEquiv.

                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def ContinuousAddEquiv.trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (cme1 : M ≃ₜ+ N) (cme2 : N ≃ₜ+ L) :

                                                                                                                                                                                        The composition of two ContinuousAddEquiv.

                                                                                                                                                                                        Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousMulEquiv.coe_trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) :
                                                                                                                                                                                            (e₁.trans e₂) = e₂ e₁
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousAddEquiv.coe_trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) :
                                                                                                                                                                                            (e₁.trans e₂) = e₂ e₁
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousMulEquiv.trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (m : M) :
                                                                                                                                                                                            (e₁.trans e₂) m = e₂ (e₁ m)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousAddEquiv.trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (m : M) :
                                                                                                                                                                                            (e₁.trans e₂) m = e₂ (e₁ m)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousMulEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (l : L) :
                                                                                                                                                                                            (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousAddEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (l : L) :
                                                                                                                                                                                            (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousMulEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) :
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousAddEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) :
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousMulEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) :
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ContinuousAddEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) :
                                                                                                                                                                                            def ContinuousMulEquiv.ofUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] :

                                                                                                                                                                                            The MulEquiv between two monoids with a unique element.

                                                                                                                                                                                            Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                def ContinuousAddEquiv.ofUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] :

                                                                                                                                                                                                The AddEquiv between two AddMonoids with a unique element.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    instance ContinuousMulEquiv.instUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] :

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

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                      instance ContinuousAddEquiv.instUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] :

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

                                                                                                                                                                                                      Equations