Additive and multiplicative equivalences associated to multiplicative
and additive
. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
add_equiv.to_multiplicative
{G : Type u_1}
{H : Type u_2}
[add_zero_class G]
[add_zero_class H] :
G ≃+ H ≃ (multiplicative G ≃* multiplicative H)
Reinterpret G ≃+ H
as multiplicative G ≃* multiplicative H
.
Equations
- add_equiv.to_multiplicative = {to_fun := λ (f : G ≃+ H), {to_fun := ⇑(⇑add_monoid_hom.to_multiplicative f.to_add_monoid_hom), inv_fun := ⇑(⇑add_monoid_hom.to_multiplicative f.symm.to_add_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}, inv_fun := λ (f : multiplicative G ≃* multiplicative H), {to_fun := ⇑(f.to_monoid_hom), inv_fun := ⇑(f.symm.to_monoid_hom), left_inv := _, right_inv := _, map_add' := _}, left_inv := _, right_inv := _}
Reinterpret G ≃* H
as additive G ≃+ additive H
.
Equations
- mul_equiv.to_additive = {to_fun := λ (f : G ≃* H), {to_fun := ⇑(⇑monoid_hom.to_additive f.to_monoid_hom), inv_fun := ⇑(⇑monoid_hom.to_additive f.symm.to_monoid_hom), left_inv := _, right_inv := _, map_add' := _}, inv_fun := λ (f : additive G ≃+ additive H), {to_fun := ⇑(f.to_add_monoid_hom), inv_fun := ⇑(f.symm.to_add_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}, left_inv := _, right_inv := _}
def
add_equiv.to_multiplicative'
{G : Type u_1}
{H : Type u_2}
[mul_one_class G]
[add_zero_class H] :
additive G ≃+ H ≃ (G ≃* multiplicative H)
Reinterpret additive G ≃+ H
as G ≃* multiplicative H
.
Equations
- add_equiv.to_multiplicative' = {to_fun := λ (f : additive G ≃+ H), {to_fun := ⇑(⇑add_monoid_hom.to_multiplicative' f.to_add_monoid_hom), inv_fun := ⇑(⇑add_monoid_hom.to_multiplicative'' f.symm.to_add_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}, inv_fun := λ (f : G ≃* multiplicative H), {to_fun := ⇑(f.to_monoid_hom), inv_fun := ⇑(f.symm.to_monoid_hom), left_inv := _, right_inv := _, map_add' := _}, left_inv := _, right_inv := _}
def
mul_equiv.to_additive'
{G : Type u_1}
{H : Type u_2}
[mul_one_class G]
[add_zero_class H] :
G ≃* multiplicative H ≃ (additive G ≃+ H)
Reinterpret G ≃* multiplicative H
as additive G ≃+ H
as.
def
add_equiv.to_multiplicative''
{G : Type u_1}
{H : Type u_2}
[add_zero_class G]
[mul_one_class H] :
G ≃+ additive H ≃ (multiplicative G ≃* H)
Reinterpret G ≃+ additive H
as multiplicative G ≃* H
.
Equations
- add_equiv.to_multiplicative'' = {to_fun := λ (f : G ≃+ additive H), {to_fun := ⇑(⇑add_monoid_hom.to_multiplicative'' f.to_add_monoid_hom), inv_fun := ⇑(⇑add_monoid_hom.to_multiplicative' f.symm.to_add_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}, inv_fun := λ (f : multiplicative G ≃* H), {to_fun := ⇑(f.to_monoid_hom), inv_fun := ⇑(f.symm.to_monoid_hom), left_inv := _, right_inv := _, map_add' := _}, left_inv := _, right_inv := _}
def
mul_equiv.to_additive''
{G : Type u_1}
{H : Type u_2}
[add_zero_class G]
[mul_one_class H] :
multiplicative G ≃* H ≃ (G ≃+ additive H)
Reinterpret multiplicative G ≃* H
as G ≃+ additive H
as.
def
add_equiv.additive_multiplicative
(G : Type u_1)
[add_zero_class G] :
additive (multiplicative G) ≃+ G
additive (multiplicative G)
is just G
.
Equations
def
mul_equiv.multiplicative_additive
(H : Type u_2)
[mul_one_class H] :
multiplicative (additive H) ≃* H
multiplicative (additive H)
is just H
.