Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2019 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes HΓΆlzl, Mario Carneiro

! This file was ported from Lean 3 source module data.rat.basic
! leanprover-community/mathlib commit a59dad53320b73ef180174aae867addd707ef00e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Field.Defs
import Mathlib.Data.Rat.Defs

/-!
# Field Structure on the Rational Numbers

## Summary

We put the (discrete) field structure on the type `β„š` of rational numbers that
was defined in `Mathlib.Data.Rat.Defs`.

## Main Definitions

- `Rat.field` is 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 `Mathlib.Data.Rat.basic β†’ Mathlib.Algebra.Field.Defs β†’ Std.Data.Rat`.

## Tags

rat, rationals, field, β„š, numerator, denominator, num, denom
-/


namespace Rat

instance 
field: Field β„š
field : 
Field: Type ?u.2 β†’ Type ?u.2
Field 
β„š: Type
β„š :=
  { 
Rat.commRing: CommRing β„š
Rat.commRing, 
Rat.commGroupWithZero: CommGroupWithZero β„š
Rat.commGroupWithZero with
    zero := 
0: ?m.123
0
    add := 
(Β· + Β·): β„š β†’ β„š β†’ β„š
(Β· + Β·)
    neg := 
Neg.neg: {Ξ± : Type ?u.471} β†’ [self : Neg Ξ±] β†’ Ξ± β†’ Ξ±
Neg.neg
    one := 
1: ?m.389
1
    mul := 
(Β· * Β·): β„š β†’ β„š β†’ β„š
(Β· * Β·)
    inv := 
Inv.inv: {Ξ± : Type ?u.599} β†’ [self : Inv Ξ±] β†’ Ξ± β†’ Ξ±
Inv.inv
    ratCast := 
Rat.cast: {K : Type ?u.687} β†’ [inst : RatCast K] β†’ β„š β†’ K
Rat.cast
    ratCast_mk := fun 
a: ?m.715
a 
b: ?m.718
b 
h1: ?m.721
h1 
h2: ?m.724
h2 => (
num_div_den: βˆ€ (r : β„š), ↑r.num / ↑r.den = r
num_div_den 
_: β„š
_).
symm: βˆ€ {Ξ± : Sort ?u.727} {a b : Ξ±}, a = b β†’ b = a
symm
    qsmul := 
(Β· * Β·): β„š β†’ β„š β†’ β„š
(Β· * Β·) }

-- Extra instances to short-circuit type class resolution
instance 
divisionRing: DivisionRing β„š
divisionRing : 
DivisionRing: Type ?u.2596 β†’ Type ?u.2596
DivisionRing 
β„š: Type
β„š := 
Goals accomplished! πŸ™
DivisionRing β„š
Goals accomplished! πŸ™


end Rat