Field structure on the multiplicative/additive opposite #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
Equations
- add_opposite.has_rat_cast α = {rat_cast := λ (n : ℚ), add_opposite.op ↑n}
@[protected, instance]
Equations
- mul_opposite.has_rat_cast α = {rat_cast := λ (n : ℚ), mul_opposite.op ↑n}
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem
add_opposite.unop_rat_cast
{α : Type u_1}
[has_rat_cast α]
(q : ℚ) :
add_opposite.unop ↑q = ↑q
@[simp, norm_cast]
theorem
mul_opposite.unop_rat_cast
{α : Type u_1}
[has_rat_cast α]
(q : ℚ) :
mul_opposite.unop ↑q = ↑q
@[protected, instance]
Equations
- mul_opposite.division_semiring α = {add := semiring.add (mul_opposite.semiring α), add_assoc := _, zero := group_with_zero.zero (mul_opposite.group_with_zero α), zero_add := _, add_zero := _, nsmul := semiring.nsmul (mul_opposite.semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := group_with_zero.mul (mul_opposite.group_with_zero α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := group_with_zero.one (mul_opposite.group_with_zero α), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (mul_opposite.semiring α), nat_cast_zero := _, nat_cast_succ := _, npow := group_with_zero.npow (mul_opposite.group_with_zero α), npow_zero' := _, npow_succ' := _, inv := group_with_zero.inv (mul_opposite.group_with_zero α), div := group_with_zero.div (mul_opposite.group_with_zero α), div_eq_mul_inv := _, zpow := group_with_zero.zpow (mul_opposite.group_with_zero α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
Equations
- mul_opposite.division_ring α = {add := division_semiring.add (mul_opposite.division_semiring α), add_assoc := _, zero := division_semiring.zero (mul_opposite.division_semiring α), zero_add := _, add_zero := _, nsmul := division_semiring.nsmul (mul_opposite.division_semiring α), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (mul_opposite.ring α), sub := ring.sub (mul_opposite.ring α), sub_eq_add_neg := _, zsmul := ring.zsmul (mul_opposite.ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (mul_opposite.ring α), nat_cast := division_semiring.nat_cast (mul_opposite.division_semiring α), one := division_semiring.one (mul_opposite.division_semiring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_semiring.mul (mul_opposite.division_semiring α), mul_assoc := _, one_mul := _, mul_one := _, npow := division_semiring.npow (mul_opposite.division_semiring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := division_semiring.inv (mul_opposite.division_semiring α), div := division_semiring.div (mul_opposite.division_semiring α), div_eq_mul_inv := _, zpow := division_semiring.zpow (mul_opposite.division_semiring α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := λ (q : ℚ), mul_opposite.op ↑q, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec (λ (q : ℚ), mul_opposite.op ↑q) (distrib.to_has_mul αᵐᵒᵖ), qsmul_eq_mul' := _}
@[protected, instance]
Equations
- mul_opposite.semifield α = {add := division_semiring.add (mul_opposite.division_semiring α), add_assoc := _, zero := division_semiring.zero (mul_opposite.division_semiring α), zero_add := _, add_zero := _, nsmul := division_semiring.nsmul (mul_opposite.division_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := division_semiring.mul (mul_opposite.division_semiring α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := division_semiring.one (mul_opposite.division_semiring α), one_mul := _, mul_one := _, nat_cast := division_semiring.nat_cast (mul_opposite.division_semiring α), nat_cast_zero := _, nat_cast_succ := _, npow := division_semiring.npow (mul_opposite.division_semiring α), npow_zero' := _, npow_succ' := _, mul_comm := _, inv := division_semiring.inv (mul_opposite.division_semiring α), div := division_semiring.div (mul_opposite.division_semiring α), div_eq_mul_inv := _, zpow := division_semiring.zpow (mul_opposite.division_semiring α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
Equations
- mul_opposite.field α = {add := division_ring.add (mul_opposite.division_ring α), add_assoc := _, zero := division_ring.zero (mul_opposite.division_ring α), zero_add := _, add_zero := _, nsmul := division_ring.nsmul (mul_opposite.division_ring α), nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg (mul_opposite.division_ring α), sub := division_ring.sub (mul_opposite.division_ring α), sub_eq_add_neg := _, zsmul := division_ring.zsmul (mul_opposite.division_ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast (mul_opposite.division_ring α), nat_cast := division_ring.nat_cast (mul_opposite.division_ring α), one := division_ring.one (mul_opposite.division_ring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_ring.mul (mul_opposite.division_ring α), mul_assoc := _, one_mul := _, mul_one := _, npow := division_ring.npow (mul_opposite.division_ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (mul_opposite.division_ring α), div := division_ring.div (mul_opposite.division_ring α), div_eq_mul_inv := _, zpow := division_ring.zpow (mul_opposite.division_ring α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast (mul_opposite.division_ring α), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul (mul_opposite.division_ring α), qsmul_eq_mul' := _}
@[protected, instance]
Equations
- add_opposite.division_semiring α = {add := semiring.add (add_opposite.semiring α), add_assoc := _, zero := group_with_zero.zero (add_opposite.group_with_zero α), zero_add := _, add_zero := _, nsmul := semiring.nsmul (add_opposite.semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := group_with_zero.mul (add_opposite.group_with_zero α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := group_with_zero.one (add_opposite.group_with_zero α), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (add_opposite.semiring α), nat_cast_zero := _, nat_cast_succ := _, npow := group_with_zero.npow (add_opposite.group_with_zero α), npow_zero' := _, npow_succ' := _, inv := group_with_zero.inv (add_opposite.group_with_zero α), div := group_with_zero.div (add_opposite.group_with_zero α), div_eq_mul_inv := _, zpow := group_with_zero.zpow (add_opposite.group_with_zero α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
Equations
- add_opposite.division_ring α = {add := ring.add (add_opposite.ring α), add_assoc := _, zero := ring.zero (add_opposite.ring α), zero_add := _, add_zero := _, nsmul := ring.nsmul (add_opposite.ring α), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (add_opposite.ring α), sub := ring.sub (add_opposite.ring α), sub_eq_add_neg := _, zsmul := ring.zsmul (add_opposite.ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (add_opposite.ring α), nat_cast := ring.nat_cast (add_opposite.ring α), one := ring.one (add_opposite.ring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (add_opposite.ring α), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (add_opposite.ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (add_opposite.group_with_zero α), div := group_with_zero.div (add_opposite.group_with_zero α), div_eq_mul_inv := _, zpow := group_with_zero.zpow (add_opposite.group_with_zero α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := has_rat_cast.rat_cast (add_opposite.has_rat_cast α), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec has_rat_cast.rat_cast (distrib.to_has_mul αᵃᵒᵖ), qsmul_eq_mul' := _}
@[protected, instance]
Equations
- add_opposite.semifield α = {add := division_semiring.add (add_opposite.division_semiring α), add_assoc := _, zero := division_semiring.zero (add_opposite.division_semiring α), zero_add := _, add_zero := _, nsmul := division_semiring.nsmul (add_opposite.division_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := division_semiring.mul (add_opposite.division_semiring α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := division_semiring.one (add_opposite.division_semiring α), one_mul := _, mul_one := _, nat_cast := division_semiring.nat_cast (add_opposite.division_semiring α), nat_cast_zero := _, nat_cast_succ := _, npow := division_semiring.npow (add_opposite.division_semiring α), npow_zero' := _, npow_succ' := _, mul_comm := _, inv := division_semiring.inv (add_opposite.division_semiring α), div := division_semiring.div (add_opposite.division_semiring α), div_eq_mul_inv := _, zpow := division_semiring.zpow (add_opposite.division_semiring α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
Equations
- add_opposite.field α = {add := division_ring.add (add_opposite.division_ring α), add_assoc := _, zero := division_ring.zero (add_opposite.division_ring α), zero_add := _, add_zero := _, nsmul := division_ring.nsmul (add_opposite.division_ring α), nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg (add_opposite.division_ring α), sub := division_ring.sub (add_opposite.division_ring α), sub_eq_add_neg := _, zsmul := division_ring.zsmul (add_opposite.division_ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast (add_opposite.division_ring α), nat_cast := division_ring.nat_cast (add_opposite.division_ring α), one := division_ring.one (add_opposite.division_ring α), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_ring.mul (add_opposite.division_ring α), mul_assoc := _, one_mul := _, mul_one := _, npow := division_ring.npow (add_opposite.division_ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (add_opposite.division_ring α), div := division_ring.div (add_opposite.division_ring α), div_eq_mul_inv := _, zpow := division_ring.zpow (add_opposite.division_ring α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast (add_opposite.division_ring α), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul (add_opposite.division_ring α), qsmul_eq_mul' := _}