logic.equiv.transfer_instance

An equivalence e : α ≃ β gives a multiplicative equivalence α ≃* β where the multiplicative structure on α is the one obtained by transporting a multiplicative structure on β back along e.

Equations

e.mul_equiv = let _inst : has_mul α := e.has_mul in {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def equiv.add_equiv {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] :

let _inst : has_add α := e.has_add in α ≃+ β

An equivalence e : α ≃ β gives a additive equivalence α ≃+ β where the additive structure on α is the one obtained by transporting an additive structure on β back along e.

Equations

e.add_equiv = let _inst : has_add α := e.has_add in {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem equiv.mul_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_mul β] (a : α) :

⇑(e.mul_equiv) a = ⇑e a

source

@[simp]

theorem equiv.add_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] (a : α) :

⇑(e.add_equiv) a = ⇑e a

source

theorem equiv.add_equiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] (b : β) :

let _inst : has_add α := e.has_add in ⇑(add_equiv.symm e.add_equiv) b = ⇑(e.symm) b

source

theorem equiv.mul_equiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_mul β] (b : β) :

let _inst : has_mul α := e.has_mul in ⇑(mul_equiv.symm e.mul_equiv) b = ⇑(e.symm) b

source

def equiv.ring_equiv {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] [has_mul β] :

let _inst : has_add α := e.has_add, _inst_3 : has_mul α := e.has_mul in α ≃+* β

An equivalence e : α ≃ β gives a ring equivalence α ≃+* β where the ring structure on α is the one obtained by transporting a ring structure on β back along e.

Equations

e.ring_equiv = let _inst : has_add α := e.has_add, _inst_3 : has_mul α := e.has_mul in {to_fun := e.to_fun, inv_fun := e.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem equiv.ring_equiv_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] [has_mul β] (a : α) :

⇑(e.ring_equiv) a = ⇑e a

source

theorem equiv.ring_equiv_symm_apply {α : Type u} {β : Type v} (e : α ≃ β) [has_add β] [has_mul β] (b : β) :

let _inst : has_add α := e.has_add, _inst_3 : has_mul α := e.has_mul in ⇑(ring_equiv.symm e.ring_equiv) b = ⇑(e.symm) b

source

@[protected, reducible]

def equiv.add_semigroup {α : Type u} {β : Type v} (e : α ≃ β) [add_semigroup β] :

add_semigroup α

Transfer add_semigroup across an equiv

Equations

e.add_semigroup = let mul : has_add α := e.has_add in function.injective.add_semigroup ⇑e _ _

source

@[protected, reducible]

def equiv.semigroup {α : Type u} {β : Type v} (e : α ≃ β) [semigroup β] :

semigroup α

Transfer semigroup across an equiv

Equations

e.semigroup = let mul : has_mul α := e.has_mul in function.injective.semigroup ⇑e _ _

source

@[protected, reducible]

def equiv.semigroup_with_zero {α : Type u} {β : Type v} (e : α ≃ β) [semigroup_with_zero β] :

semigroup_with_zero α

Transfer semigroup_with_zero across an equiv

Equations

e.semigroup_with_zero = let mul : has_mul α := e.has_mul, zero : has_zero α := e.has_zero in function.injective.semigroup_with_zero ⇑e _ _ _

source

@[protected, reducible]

def equiv.comm_semigroup {α : Type u} {β : Type v} (e : α ≃ β) [comm_semigroup β] :

comm_semigroup α

Transfer comm_semigroup across an equiv

Equations

e.comm_semigroup = let mul : has_mul α := e.has_mul in function.injective.comm_semigroup ⇑e _ _

source

@[protected, reducible]

def equiv.add_comm_semigroup {α : Type u} {β : Type v} (e : α ≃ β) [add_comm_semigroup β] :

add_comm_semigroup α

Transfer add_comm_semigroup across an equiv

Equations

e.add_comm_semigroup = let mul : has_add α := e.has_add in function.injective.add_comm_semigroup ⇑e _ _

source

@[protected, reducible]

def equiv.mul_zero_class {α : Type u} {β : Type v} (e : α ≃ β) [mul_zero_class β] :

mul_zero_class α

Transfer mul_zero_class across an equiv

Equations

e.mul_zero_class = let zero : has_zero α := e.has_zero, mul : has_mul α := e.has_mul in function.injective.mul_zero_class ⇑e _ _ _

source

@[protected, reducible]

def equiv.mul_one_class {α : Type u} {β : Type v} (e : α ≃ β) [mul_one_class β] :

mul_one_class α

Transfer mul_one_class across an equiv

Equations

e.mul_one_class = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.mul_one_class ⇑e _ _ _

source

@[protected, reducible]

def equiv.add_zero_class {α : Type u} {β : Type v} (e : α ≃ β) [add_zero_class β] :

add_zero_class α

Transfer add_zero_class across an equiv

Equations

e.add_zero_class = let one : has_zero α := e.has_zero, mul : has_add α := e.has_add in function.injective.add_zero_class ⇑e _ _ _

source

@[protected, reducible]

def equiv.mul_zero_one_class {α : Type u} {β : Type v} (e : α ≃ β) [mul_zero_one_class β] :

mul_zero_one_class α

Transfer mul_zero_one_class across an equiv

Equations

e.mul_zero_one_class = let zero : has_zero α := e.has_zero, one : has_one α := e.has_one, mul : has_mul α := e.has_mul in function.injective.mul_zero_one_class ⇑e _ _ _ _

source

@[protected, reducible]

def equiv.add_monoid {α : Type u} {β : Type v} (e : α ≃ β) [add_monoid β] :

add_monoid α

Transfer add_monoid across an equiv

Equations

e.add_monoid = let one : has_zero α := e.has_zero, mul : has_add α := e.has_add, pow : has_smul ℕ α := e.has_smul ℕ in function.injective.add_monoid ⇑e _ _ _ _

source

@[protected, reducible]

def equiv.monoid {α : Type u} {β : Type v} (e : α ≃ β) [monoid β] :

monoid α

Transfer monoid across an equiv

Equations

e.monoid = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, pow : has_pow α ℕ := e.has_pow ℕ in function.injective.monoid ⇑e _ _ _ _

source

@[protected, reducible]

def equiv.comm_monoid {α : Type u} {β : Type v} (e : α ≃ β) [comm_monoid β] :

comm_monoid α

Transfer comm_monoid across an equiv

Equations

e.comm_monoid = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, pow : has_pow α ℕ := e.has_pow ℕ in function.injective.comm_monoid ⇑e _ _ _ _

source

@[protected, reducible]

def equiv.add_comm_monoid {α : Type u} {β : Type v} (e : α ≃ β) [add_comm_monoid β] :

add_comm_monoid α

Transfer add_comm_monoid across an equiv

Equations

e.add_comm_monoid = let one : has_zero α := e.has_zero, mul : has_add α := e.has_add, pow : has_smul ℕ α := e.has_smul ℕ in function.injective.add_comm_monoid ⇑e _ _ _ _

source

@[protected, reducible]

def equiv.group {α : Type u} {β : Type v} (e : α ≃ β) [group β] :

group α

Transfer group across an equiv

Equations

e.group = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, inv : has_inv α := e.has_inv, div : has_div α := e.has_div, npow : has_pow α ℕ := e.has_pow ℕ, zpow : has_pow α ℤ := e.has_pow ℤ in function.injective.group ⇑e _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.add_group {α : Type u} {β : Type v} (e : α ≃ β) [add_group β] :

add_group α

Transfer add_group across an equiv

Equations

e.add_group = let one : has_zero α := e.has_zero, mul : has_add α := e.has_add, inv : has_neg α := e.has_neg, div : has_sub α := e.has_sub, npow : has_smul ℕ α := e.has_smul ℕ, zpow : has_smul ℤ α := e.has_smul ℤ in function.injective.add_group ⇑e _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.add_comm_group {α : Type u} {β : Type v} (e : α ≃ β) [add_comm_group β] :

add_comm_group α

Transfer add_comm_group across an equiv

Equations

e.add_comm_group = let one : has_zero α := e.has_zero, mul : has_add α := e.has_add, inv : has_neg α := e.has_neg, div : has_sub α := e.has_sub, npow : has_smul ℕ α := e.has_smul ℕ, zpow : has_smul ℤ α := e.has_smul ℤ in function.injective.add_comm_group ⇑e _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.comm_group {α : Type u} {β : Type v} (e : α ≃ β) [comm_group β] :

comm_group α

Transfer comm_group across an equiv

Equations

e.comm_group = let one : has_one α := e.has_one, mul : has_mul α := e.has_mul, inv : has_inv α := e.has_inv, div : has_div α := e.has_div, npow : has_pow α ℕ := e.has_pow ℕ, zpow : has_pow α ℤ := e.has_pow ℤ in function.injective.comm_group ⇑e _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_non_assoc_semiring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_non_assoc_semiring β] :

non_unital_non_assoc_semiring α

Transfer non_unital_non_assoc_semiring across an equiv

Equations

e.non_unital_non_assoc_semiring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, nsmul : has_smul ℕ α := e.has_smul ℕ in function.injective.non_unital_non_assoc_semiring ⇑e _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_semiring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_semiring β] :

non_unital_semiring α

Transfer non_unital_semiring across an equiv

Equations

e.non_unital_semiring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, nsmul : has_smul ℕ α := e.has_smul ℕ in function.injective.non_unital_semiring ⇑e _ _ _ _ _

source

@[protected, reducible]

def equiv.add_monoid_with_one {α : Type u} {β : Type v} (e : α ≃ β) [add_monoid_with_one β] :

add_monoid_with_one α

Transfer add_monoid_with_one across an equiv

Equations

e.add_monoid_with_one = {nat_cast := λ (n : ℕ), ⇑(e.symm) ↑n, add := add_monoid.add e.add_monoid, add_assoc := _, zero := add_monoid.zero e.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul e.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}

source

@[protected, reducible]

def equiv.add_group_with_one {α : Type u} {β : Type v} (e : α ≃ β) [add_group_with_one β] :

add_group_with_one α

Transfer add_group_with_one across an equiv

Equations

e.add_group_with_one = {int_cast := λ (n : ℤ), ⇑(e.symm) ↑n, add := add_monoid_with_one.add e.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero e.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul e.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg e.add_group, sub := add_group.sub e.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul e.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := add_monoid_with_one.nat_cast e.add_monoid_with_one, one := add_monoid_with_one.one e.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[protected, reducible]

def equiv.non_assoc_semiring {α : Type u} {β : Type v} (e : α ≃ β) [non_assoc_semiring β] :

non_assoc_semiring α

Transfer non_assoc_semiring across an equiv

Equations

e.non_assoc_semiring = let mul : has_mul α := e.has_mul, add_monoid_with_one_1 : add_monoid_with_one α := e.add_monoid_with_one in function.injective.non_assoc_semiring ⇑e _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.semiring {α : Type u} {β : Type v} (e : α ≃ β) [semiring β] :

semiring α

Transfer semiring across an equiv

Equations

e.semiring = let mul : has_mul α := e.has_mul, add_monoid_with_one_1 : add_monoid_with_one α := e.add_monoid_with_one, npow : has_pow α ℕ := e.has_pow ℕ in function.injective.semiring ⇑e _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_comm_semiring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_comm_semiring β] :

non_unital_comm_semiring α

Transfer non_unital_comm_semiring across an equiv

Equations

e.non_unital_comm_semiring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, nsmul : has_smul ℕ α := e.has_smul ℕ in function.injective.non_unital_comm_semiring ⇑e _ _ _ _ _

source

@[protected, reducible]

def equiv.comm_semiring {α : Type u} {β : Type v} (e : α ≃ β) [comm_semiring β] :

comm_semiring α

Transfer comm_semiring across an equiv

Equations

e.comm_semiring = let mul : has_mul α := e.has_mul, add_monoid_with_one_1 : add_monoid_with_one α := e.add_monoid_with_one, npow : has_pow α ℕ := e.has_pow ℕ in function.injective.comm_semiring ⇑e _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_non_assoc_ring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_non_assoc_ring β] :

non_unital_non_assoc_ring α

Transfer non_unital_non_assoc_ring across an equiv

Equations

e.non_unital_non_assoc_ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub, nsmul : has_smul ℕ α := e.has_smul ℕ, zsmul : has_smul ℤ α := e.has_smul ℤ in function.injective.non_unital_non_assoc_ring ⇑e _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_ring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_ring β] :

non_unital_ring α

Transfer non_unital_ring across an equiv

Equations

e.non_unital_ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub, nsmul : has_smul ℕ α := e.has_smul ℕ, zsmul : has_smul ℤ α := e.has_smul ℤ in function.injective.non_unital_ring ⇑e _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_assoc_ring {α : Type u} {β : Type v} (e : α ≃ β) [non_assoc_ring β] :

non_assoc_ring α

Transfer non_assoc_ring across an equiv

Equations

e.non_assoc_ring = let add_group_with_one_1 : add_group_with_one α := e.add_group_with_one, mul : has_mul α := e.has_mul in function.injective.non_assoc_ring ⇑e _ _ _ _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.ring {α : Type u} {β : Type v} (e : α ≃ β) [ring β] :

ring α

Transfer ring across an equiv

Equations

e.ring = let mul : has_mul α := e.has_mul, add_group_with_one_1 : add_group_with_one α := e.add_group_with_one, npow : has_pow α ℕ := e.has_pow ℕ in function.injective.ring ⇑e _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.non_unital_comm_ring {α : Type u} {β : Type v} (e : α ≃ β) [non_unital_comm_ring β] :

non_unital_comm_ring α

Transfer non_unital_comm_ring across an equiv

Equations

e.non_unital_comm_ring = let zero : has_zero α := e.has_zero, add : has_add α := e.has_add, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, sub : has_sub α := e.has_sub, nsmul : has_smul ℕ α := e.has_smul ℕ, zsmul : has_smul ℤ α := e.has_smul ℤ in function.injective.non_unital_comm_ring ⇑e _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.comm_ring {α : Type u} {β : Type v} (e : α ≃ β) [comm_ring β] :

comm_ring α

Transfer comm_ring across an equiv

Equations

e.comm_ring = let mul : has_mul α := e.has_mul, add_group_with_one_1 : add_group_with_one α := e.add_group_with_one, npow : has_pow α ℕ := e.has_pow ℕ in function.injective.comm_ring ⇑e _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, reducible]

theorem equiv.nontrivial {α : Type u} {β : Type v} (e : α ≃ β) [nontrivial β] :

nontrivial α

Transfer nontrivial across an equiv

source

@[protected, reducible]

theorem equiv.is_domain {α : Type u} {β : Type v} [ring α] [ring β] [is_domain β] (e : α ≃+* β) :

is_domain α

Transfer is_domain across an equiv

source

@[protected, reducible]

def equiv.has_rat_cast {α : Type u} {β : Type v} (e : α ≃ β) [has_rat_cast β] :

has_rat_cast α

Transfer has_rat_cast across an equiv

Equations

e.has_rat_cast = {rat_cast := λ (n : ℚ), ⇑(e.symm) ↑n}

source

@[protected, reducible]

def equiv.division_ring {α : Type u} {β : Type v} (e : α ≃ β) [division_ring β] :

division_ring α

Transfer division_ring across an equiv

Equations

e.division_ring = let add_group_with_one_1 : add_group_with_one α := e.add_group_with_one, mul : has_mul α := e.has_mul, inv : has_inv α := e.has_inv, div : has_div α := e.has_div, mul : has_mul α := e.has_mul, npow : has_pow α ℕ := e.has_pow ℕ, zpow : has_pow α ℤ := e.has_pow ℤ, rat_cast : has_rat_cast α := e.has_rat_cast, qsmul : has_smul ℚ α := e.has_smul ℚ in function.injective.division_ring ⇑e _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.field {α : Type u} {β : Type v} (e : α ≃ β) [field β] :

field α

Transfer field across an equiv

Equations

e.field = let add_group_with_one_1 : add_group_with_one α := e.add_group_with_one, mul : has_mul α := e.has_mul, neg : has_neg α := e.has_neg, inv : has_inv α := e.has_inv, div : has_div α := e.has_div, mul : has_mul α := e.has_mul, npow : has_pow α ℕ := e.has_pow ℕ, zpow : has_pow α ℤ := e.has_pow ℤ, rat_cast : has_rat_cast α := e.has_rat_cast, qsmul : has_smul ℚ α := e.has_smul ℚ in function.injective.field ⇑e _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

source

@[protected, reducible]

def equiv.mul_action {α : Type u} {β : Type v} (R : Type u_1) [monoid R] (e : α ≃ β) [mul_action R β] :

mul_action R α

Transfer mul_action across an equiv

Equations

equiv.mul_action R e = {to_has_smul := {smul := has_smul.smul (e.has_smul R)}, one_smul := _, mul_smul := _}

source

@[protected, reducible]

def equiv.distrib_mul_action {α : Type u} {β : Type v} (R : Type u_1) [monoid R] (e : α ≃ β) [add_comm_monoid β] :

let _inst : add_comm_monoid α := e.add_comm_monoid in Π [_inst_3 : distrib_mul_action R β], distrib_mul_action R α

Transfer distrib_mul_action across an equiv

Equations

equiv.distrib_mul_action R e = let _inst : add_comm_monoid α := e.add_comm_monoid in λ (_inst_3 : distrib_mul_action R β), let _inst_4 : add_comm_monoid α := e.add_comm_monoid in {to_mul_action := {to_has_smul := mul_action.to_has_smul (equiv.mul_action R e), one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

source

@[protected, reducible]

def equiv.module {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α ≃ β) [add_comm_monoid β] :

let _inst : add_comm_monoid α := e.add_comm_monoid in Π [_inst_3 : module R β], module R α

Transfer module across an equiv

Equations

equiv.module R e = let _inst : add_comm_monoid α := e.add_comm_monoid in λ (_inst_3 : module R β), {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (equiv.distrib_mul_action R e), smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

source

def equiv.linear_equiv {α : Type u} {β : Type v} (R : Type u_1) [semiring R] (e : α ≃ β) [add_comm_monoid β] [module R β] :

let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : module R α := equiv.module R e in α ≃ₗ[R] β

An equivalence e : α ≃ β gives a linear equivalence α ≃ₗ[R] β where the R-module structure on α is the one obtained by transporting an R-module structure on β back along e.

Equations

equiv.linear_equiv R e = let _inst : add_comm_monoid α := e.add_comm_monoid, _inst_4 : module R α := equiv.module R e in {to_fun := e.add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := e.add_equiv.inv_fun, left_inv := _, right_inv := _}

source

@[protected, reducible]

def equiv.algebra {α : Type u} {β : Type v} (R : Type u_1) [comm_semiring R] (e : α ≃ β) [semiring β] :

let _inst : semiring α := e.semiring in Π [_inst_3 : algebra R β], algebra R α

Transfer algebra across an equiv

Equations

equiv.algebra R e = let _inst : semiring α := e.semiring in λ (_inst_3 : algebra R β), (↑(ring_equiv.symm e.ring_equiv).comp (algebra_map R β)).to_algebra' _

source

def equiv.alg_equiv {α : Type u} {β : Type v} (R : Type u_1) [comm_semiring R] (e : α ≃ β) [semiring β] [algebra R β] :

let _inst : semiring α := e.semiring, _inst_4 : algebra R α := equiv.algebra R e in α ≃ₐ[R] β

An equivalence e : α ≃ β gives an algebra equivalence α ≃ₐ[R] β where the R-algebra structure on α is the one obtained by transporting an R-algebra structure on β back along e.

Equations

equiv.alg_equiv R e = let _inst : semiring α := e.semiring, _inst_4 : algebra R α := equiv.algebra R e in {to_fun := e.ring_equiv.to_fun, inv_fun := e.ring_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

mathlib3 documentation

Transfer algebraic structures across `equiv`s #

Implementation details #

Tags #

Transfer algebraic structures across equivs #

Implementation details #

Tags #

Transfer algebraic structures across `equiv`s #