Field Structure on the Rational Numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Summary #
We put the (discrete) field structure on the type ℚ of rational numbers that
was defined in data.rat.defs.
Main Definitions #
rat.fieldis the field structure onℚ.
Implementation notes #
We have to define the field structure in a separate file to avoid cyclic imports:
the field class contains a map from ℚ (see field's docstring for the rationale),
so we have a dependency rat.field → field → rat that is reflected in the import
hierarchy data.rat.basic → algebra.field.basic → data.rat.defs.
Tags #
rat, rationals, field, ℚ, numerator, denominator, num, denom
@[protected, instance]
Equations
- rat.field = {add := has_add.add rat.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul rat.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg rat.has_neg, sub := comm_ring.sub rat.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul rat.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast rat.comm_ring, nat_cast := comm_ring.nat_cast rat.comm_ring, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul rat.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow rat.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv rat.has_inv, div := comm_group_with_zero.div rat.comm_group_with_zero, div_eq_mul_inv := _, zpow := comm_group_with_zero.zpow rat.comm_group_with_zero, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := id ℚ, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := rat.field._proof_1, qsmul := has_mul.mul rat.has_mul, qsmul_eq_mul' := rat.field._proof_2}
@[protected, instance]