Instances for Euclidean domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
int.euclidean_domain: shows thatℤis a Euclidean domain.field.to_euclidean_domain: shows that any field is a Euclidean domain.
@[protected, instance]
Equations
- int.euclidean_domain = {to_comm_ring := {add := has_add.add int.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul int.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg int.has_neg, sub := comm_ring.sub int.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul int.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast int.comm_ring, nat_cast := comm_ring.nat_cast int.comm_ring, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul int.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow int.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := int.euclidean_domain._proof_1, quotient := has_div.div int.has_div, quotient_zero := int.div_zero, remainder := has_mod.mod int.has_mod, quotient_mul_add_remainder_eq := int.euclidean_domain._proof_2, r := λ (a b : ℤ), a.nat_abs < b.nat_abs, r_well_founded := int.euclidean_domain._proof_3, remainder_lt := int.euclidean_domain._proof_4, mul_left_not_lt := int.euclidean_domain._proof_5}
@[protected, instance]
Equations
- field.to_euclidean_domain = {to_comm_ring := {add := has_add.add (distrib.to_has_add K), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := field.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg K), sub := field.sub _inst_1, sub_eq_add_neg := _, zsmul := field.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast _inst_1, nat_cast := field.nat_cast _inst_1, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (distrib.to_has_mul K), mul_assoc := _, one_mul := _, mul_one := _, npow := field.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := _, quotient := has_div.div (div_inv_monoid.to_has_div K), quotient_zero := _, remainder := λ (a b : K), a - a * b / b, quotient_mul_add_remainder_eq := _, r := λ (a b : K), a = 0 ∧ b ≠ 0, r_well_founded := _, remainder_lt := _, mul_left_not_lt := _}