class Hex.Fraction.NonzeroOne (R : Type u) [Zero R] [One R] : Prop

The nontriviality needed to use 1 as a fraction denominator. Brown's nonzero input hypothesis supplies this locally even though the lightweight commutative-ring hierarchy itself permits the trivial ring.

• one_ne_zero : 1 ≠ 0

theorem Hex.Fraction.NonzeroOne.of_ne_zero {R : Type u} [Lean.Grind.CommRing R] {a : R} (ha : a ≠ 0) : NonzeroOne R

Any nonzero element of a commutative ring witnesses its nontriviality.

structure Hex.Fraction.Rep (R : Type u) [Zero R] : Type u

A numerator and a certified nonzero denominator.

• num : R

  The numerator.

• den : R

  The denominator.

• den_ne : self.den ≠ 0

  The denominator is nonzero, so the quotient is well defined.

def Hex.Fraction.Rep.Rel {R : Type u} [Lean.Grind.CommRing R] (a b : Rep R) : Prop

Cross-multiplication equivalence on fraction representatives.

Equations

• a.Rel b = (a.num * b.den = b.num * a.den)

theorem Hex.Fraction.Rep.rel_refl {R : Type u} [Lean.Grind.CommRing R] (a : Rep R) : a.Rel a

Cross-multiplication is reflexive.

theorem Hex.Fraction.Rep.rel_symm {R : Type u} [Lean.Grind.CommRing R] {a b : Rep R} (h : a.Rel b) : b.Rel a

Cross-multiplication is symmetric.

theorem Hex.Fraction.Rep.rel_trans {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {a b c : Rep R} (hab : a.Rel b) (hbc : b.Rel c) : a.Rel c

Cross-multiplication is transitive; cancellation by the nonzero middle denominator is where ExactDivLaws enters.

@[instance_reducible]

instance Hex.Fraction.Rep.instSetoid {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Setoid (Rep R)

Fraction representatives form a setoid under cross multiplication.

Equations

• Hex.Fraction.Rep.instSetoid = { r := Hex.Fraction.Rep.Rel, iseqv := ⋯ }

@[instance_reducible]

instance Hex.Fraction.Rep.instDecidableRelOfDecidableEq {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (a b : Rep R) : Decidable (a.Rel b)

Cross-multiplication equivalence is decidable when coefficient equality is.

Equations

• a.instDecidableRelOfDecidableEq b = id inferInstance

def Hex.Fraction.Rep.mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Rep R) : Rep R

Product of two representatives.

Equations

• a.mul b = { num := a.num * b.num, den := a.den * b.den, den_ne := ⋯ }

def Hex.Fraction.Rep.add {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Rep R) : Rep R

Sum of two representatives.

Equations

• a.add b = { num := a.num * b.den + b.num * a.den, den := a.den * b.den, den_ne := ⋯ }

def Hex.Fraction.Rep.neg {R : Type u} [Lean.Grind.CommRing R] (a : Rep R) : Rep R

Additive inverse of a representative.

Equations

• a.neg = { num := -a.num, den := a.den, den_ne := ⋯ }

theorem Hex.Fraction.Rep.mul_rel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {a b c d : Rep R} (hac : a.Rel c) (hbd : b.Rel d) : (a.mul b).Rel (c.mul d)

Representative products respect cross-multiplication equivalence.

theorem Hex.Fraction.Rep.add_rel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {a b c d : Rep R} (hac : a.Rel c) (hbd : b.Rel d) : (a.add b).Rel (c.add d)

Representative sums respect cross-multiplication equivalence.

theorem Hex.Fraction.Rep.neg_rel {R : Type u} [Lean.Grind.CommRing R] {a b : Rep R} (hab : a.Rel b) : a.neg.Rel b.neg

Representative negation respects cross-multiplication equivalence.

def Hex.Fraction (R : Type u) [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Type u

The quotient field of a commutative exact-division domain.

Equations

• Hex.Fraction R = Quotient Hex.Fraction.Rep.instSetoid

@[instance_reducible]

instance Hex.Fraction.instDecidableEq {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [DecidableEq R] : DecidableEq (Fraction R)

Decidable equality inherited from cross multiplication of representatives.

Equations

• q₁.instDecidableEq q₂ = Quotient.recOnSubsingleton₂ q₁ q₂ fun (a b : Hex.Fraction.Rep R) => if h : a.Rel b then isTrue ⋯ else isFalse ⋯

def Hex.Fraction.ofRep {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a : Rep R) : Fraction R

Inject a representative into its quotient.

Equations

• Hex.Fraction.ofRep a = Quotient.mk Hex.Fraction.Rep.instSetoid a

def Hex.Fraction.ofCoeff {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : R) : Fraction R

Embed a coefficient as a fraction with denominator one.

Equations

• Hex.Fraction.ofCoeff a = Hex.Fraction.ofRep { num := a, den := 1, den_ne := ⋯ }

def Hex.Fraction.mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Fraction R → Fraction R → Fraction R

Multiplication of fractions.

Equations

• Hex.Fraction.mul = Quotient.lift₂ (fun (a b : Hex.Fraction.Rep R) => Hex.Fraction.ofRep (a.mul b)) ⋯

def Hex.Fraction.add {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Fraction R → Fraction R → Fraction R

Addition of fractions.

Equations

• Hex.Fraction.add = Quotient.lift₂ (fun (a b : Hex.Fraction.Rep R) => Hex.Fraction.ofRep (a.add b)) ⋯

def Hex.Fraction.neg {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Fraction R → Fraction R

Negation of fractions.

Equations

• Hex.Fraction.neg = Quotient.lift (fun (a : Hex.Fraction.Rep R) => Hex.Fraction.ofRep a.neg) ⋯

@[instance_reducible]

instance Hex.Fraction.instZero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : Zero (Fraction R)

Zero is the embedded coefficient zero.

Equations

• Hex.Fraction.instZero = { zero := Hex.Fraction.ofCoeff 0 }

@[instance_reducible]

instance Hex.Fraction.instOne {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : One (Fraction R)

One is the embedded coefficient one.

Equations

• Hex.Fraction.instOne = { one := Hex.Fraction.ofCoeff 1 }

@[instance_reducible]

instance Hex.Fraction.instAdd {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Add (Fraction R)

Addition of fractions.

Equations

• Hex.Fraction.instAdd = { add := Hex.Fraction.add }

@[instance_reducible]

instance Hex.Fraction.instMul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Mul (Fraction R)

Multiplication of fractions.

Equations

• Hex.Fraction.instMul = { mul := Hex.Fraction.mul }

@[instance_reducible]

instance Hex.Fraction.instNeg {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Neg (Fraction R)

Negation of fractions.

Equations

• Hex.Fraction.instNeg = { neg := Hex.Fraction.neg }

@[instance_reducible]

instance Hex.Fraction.instSub {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] : Sub (Fraction R)

Subtraction of fractions, defined as addition of the negation.

Equations

• Hex.Fraction.instSub = { sub := fun (a b : Hex.Fraction R) => a + -b }

theorem Hex.Fraction.add_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : a + 0 = a

Zero is a right additive identity.

theorem Hex.Fraction.add_comm {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Fraction R) : a + b = b + a

Fraction addition is commutative.

theorem Hex.Fraction.add_assoc {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b c : Fraction R) : a + b + c = a + (b + c)

Fraction addition is associative.

theorem Hex.Fraction.mul_assoc {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b c : Fraction R) : a * b * c = a * (b * c)

Fraction multiplication is associative.

theorem Hex.Fraction.mul_one {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : a * 1 = a

One is a right multiplicative identity.

theorem Hex.Fraction.one_mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : 1 * a = a

One is a left multiplicative identity.

theorem Hex.Fraction.left_distrib {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b c : Fraction R) : a * (b + c) = a * b + a * c

Fraction multiplication distributes over addition on the left.

theorem Hex.Fraction.right_distrib {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b c : Fraction R) : (a + b) * c = a * c + b * c

Fraction multiplication distributes over addition on the right.

theorem Hex.Fraction.zero_mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : 0 * a = 0

Zero is a left multiplicative absorber.

theorem Hex.Fraction.mul_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : a * 0 = 0

Zero is a right multiplicative absorber.

theorem Hex.Fraction.neg_add_cancel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : -a + a = 0

Every fraction cancels with its negation.

theorem Hex.Fraction.neg_neg {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a : Fraction R) : - -a = a

Fraction negation is involutive.

theorem Hex.Fraction.mul_comm {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Fraction R) : a * b = b * a

Fraction multiplication is commutative.

theorem Hex.Fraction.neg_mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Fraction R) : -a * b = -(a * b)

Negation moves out of the left factor of a product.

@[simp]

theorem Hex.Fraction.ofCoeff_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : ofCoeff Zero.zero = Zero.zero

The coefficient embedding preserves zero.

@[simp]

theorem Hex.Fraction.ofCoeff_one {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : ofCoeff One.one = One.one

The coefficient embedding preserves one.

@[simp]

theorem Hex.Fraction.ofCoeff_add {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a b : R) : ofCoeff (a + b) = ofCoeff a + ofCoeff b

The coefficient embedding preserves addition.

@[simp]

theorem Hex.Fraction.ofCoeff_mul {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a b : R) : ofCoeff (a * b) = ofCoeff a * ofCoeff b

The coefficient embedding preserves multiplication.

@[simp]

theorem Hex.Fraction.ofCoeff_neg {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : R) : ofCoeff (-a) = -ofCoeff a

The coefficient embedding preserves negation.

@[simp]

theorem Hex.Fraction.ofCoeff_sub {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a b : R) : ofCoeff (a - b) = ofCoeff a - ofCoeff b

The coefficient embedding preserves subtraction.

theorem Hex.Fraction.ofCoeff_injective {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] {a b : R} (h : ofCoeff a = ofCoeff b) : a = b

The coefficient embedding is injective.

def Hex.Fraction.natPow {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Fraction R) : Nat → Fraction R

Natural powers of fractions.

Equations

• a.natPow 0 = 1
• a.natPow n.succ = a.natPow n * a

@[instance_reducible]

instance Hex.Fraction.instNatCast {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : NatCast (Fraction R)

Natural-number casts factor through the coefficient embedding.

Equations

• Hex.Fraction.instNatCast = { natCast := fun (n : Nat) => Hex.Fraction.ofCoeff ↑n }

@[instance_reducible]

instance Hex.Fraction.instOfNat {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (n : Nat) : OfNat (Fraction R) n

Numerals factor through the coefficient embedding, reusing the canonical zero and one.

Equations

• Hex.Fraction.instOfNat 0 = { ofNat := Zero.zero }
• Hex.Fraction.instOfNat 1 = { ofNat := One.one }
• Hex.Fraction.instOfNat n_2.succ.succ = { ofNat := Hex.Fraction.ofCoeff (OfNat.ofNat (n_2 + 2)) }

theorem Hex.Fraction.ofNat_eq_ofCoeff {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (n : Nat) : OfNat.ofNat n = ofCoeff (OfNat.ofNat n)

Fraction numerals agree with embedded coefficient numerals.

@[instance_reducible]

instance Hex.Fraction.instSMulNat {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : SMul Nat (Fraction R)

Natural scalar multiplication is multiplication by the cast scalar.

Equations

• Hex.Fraction.instSMulNat = { smul := fun (n : Nat) (a : Hex.Fraction R) => ↑n * a }

@[instance_reducible]

instance Hex.Fraction.instHPowNat {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : HPow (Fraction R) Nat (Fraction R)

Natural powers of fractions via natPow.

Equations

• Hex.Fraction.instHPowNat = { hPow := Hex.Fraction.natPow }

@[instance_reducible]

instance Hex.Fraction.instIntCast {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : IntCast (Fraction R)

Integer casts factor through the coefficient embedding.

Equations

• Hex.Fraction.instIntCast = { intCast := fun (i : Int) => Hex.Fraction.ofCoeff ↑i }

@[instance_reducible]

instance Hex.Fraction.instSMulInt {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : SMul Int (Fraction R)

Integer scalar multiplication is multiplication by the cast scalar.

Equations

• Hex.Fraction.instSMulInt = { smul := fun (i : Int) (a : Hex.Fraction R) => ↑i * a }

@[instance_reducible]

instance Hex.Fraction.instSemiring {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : Lean.Grind.Semiring (Fraction R)

The quotient construction is a lightweight semiring.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Fraction.instRing {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : Lean.Grind.Ring (Fraction R)

The quotient construction is a lightweight ring.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Fraction.instCommRing {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : Lean.Grind.CommRing (Fraction R)

The quotient construction is a lightweight commutative ring.

Equations

• Hex.Fraction.instCommRing = { toRing := Hex.Fraction.instRing, mul_comm := ⋯ }

def Hex.Fraction.invRep {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a : Rep R) : Fraction R

Reciprocal of a fraction representative, with zero sent to zero.

Equations

• Hex.Fraction.invRep a = if h : a.num = 0 then 0 else Hex.Fraction.ofRep { num := a.den, den := a.num, den_ne := h }

def Hex.Fraction.inv {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : Fraction R → Fraction R

Multiplicative inverse in the fraction field.

Equations

• Hex.Fraction.inv = Quotient.lift Hex.Fraction.invRep ⋯

@[instance_reducible]

instance Hex.Fraction.instInv {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : Inv (Fraction R)

Total inversion of fractions, with zero sent to zero.

Equations

• Hex.Fraction.instInv = { inv := Hex.Fraction.inv }

@[instance_reducible]

instance Hex.Fraction.instDiv {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : Div (Fraction R)

Division of fractions is multiplication by the total inverse.

Equations

• Hex.Fraction.instDiv = { div := fun (a b : Hex.Fraction R) => a * b⁻¹ }

@[simp]

theorem Hex.Fraction.mul_ofRep {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (a b : Rep R) : ofRep a * ofRep b = ofRep (a.mul b)

Products of embedded representatives multiply representatives.

theorem Hex.Fraction.ofRep_mul_den {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Rep R) : ofRep a * ofCoeff a.den = ofCoeff a.num

Multiplying a represented fraction by its embedded denominator recovers its embedded numerator.

@[simp]

theorem Hex.Fraction.inv_ofRep {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a : Rep R) : (ofRep a)⁻¹ = invRep a

Inverting an embedded representative applies invRep.

theorem Hex.Fraction.ofRep_eq_zero_iff {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : Rep R) : ofRep a = 0 ↔ a.num = 0

A representative is zero exactly when its numerator is zero.

@[simp]

theorem Hex.Fraction.ofCoeff_eq_zero_iff {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : R) : ofCoeff a = 0 ↔ a = 0

The coefficient embedding reflects zero.

@[simp]

theorem Hex.Fraction.inv_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : 0⁻¹ = 0

Fraction inversion uses the stable zero branch.

theorem Hex.Fraction.mul_inv_cancel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] {a : Fraction R} (ha : a ≠ 0) : a * a⁻¹ = 1

Every nonzero fraction has the expected multiplicative inverse.

theorem Hex.Fraction.zero_ne_one {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] : 0 ≠ 1

Zero and one are distinct in the fraction field.

theorem Hex.Fraction.inv_inv {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a : Fraction R) : a⁻¹⁻¹ = a

Inversion is involutive.

theorem Hex.Fraction.inv_one {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : 1⁻¹ = 1

The inverse of one is one.

def Hex.Fraction.intPow {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a : Fraction R) : Int → Fraction R

Integer powers of fractions use natural powers and total inversion.

Equations

• a.intPow (Int.ofNat n) = a ^ n
• a.intPow (Int.negSucc n) = (a ^ (n + 1))⁻¹

@[instance_reducible]

instance Hex.Fraction.instHPowInt {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : HPow (Fraction R) Int (Fraction R)

Integer powers of fractions via intPow.

Equations

• Hex.Fraction.instHPowInt = { hPow := Hex.Fraction.intPow }

theorem Hex.Fraction.div_eq_mul_inv {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a b : Fraction R) : a / b = a * b⁻¹

Division is multiplication by the fraction inverse.

theorem Hex.Fraction.div_mul_cancel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (a : Fraction R) {b : Fraction R} (hb : b ≠ 0) : a / b * b = a

A nonzero denominator cancels on the right of fraction division.

instance Hex.Fraction.instExactDivLaws {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : ExactDivLaws (Fraction R)

Fraction division satisfies the exact-division law.

@[instance_reducible]

instance Hex.Fraction.instField {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] : Lean.Grind.Field (Fraction R)

The quotient construction is a field in the lightweight Grind hierarchy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.Fraction.ofCoeff_pow {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] (a : R) (n : Nat) : ofCoeff (a ^ n) = ofCoeff a ^ n

The coefficient embedding preserves natural powers.

theorem Hex.Fraction.div_pullback {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] {a b c : R} (hb : b ≠ 0) (h : ofCoeff c = ofCoeff a / ofCoeff b) : a / b = c

Pull an exact scalar quotient back through the coefficient embedding.

The hypothesis that the fraction quotient lies in the image is the integrality fact supplied by generalized subresultants.

theorem Hex.Fraction.div_exact {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] {a b : R} (hb : b ≠ 0) (h : ∃ (c : R), ofCoeff c = ofCoeff a / ofCoeff b) : a / b * b = a

An integral fraction quotient reconstructs its numerator in the original coefficient ring.

theorem Hex.Fraction.exactDiv_exact {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] {a b : R} (hb : b ≠ 0) (h : ∃ (c : R), ofCoeff c = ofCoeff a / ofCoeff b) : exactDiv a b * b = a

The total exact-division wrapper reconstructs a nonzero-denominator numerator whenever its fraction quotient is integral.

theorem Hex.Fraction.divExp_exact {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] [NonzeroOne R] [DecidableEq R] (x y : R) (n : Nat) (hden : powNat y (n - 1) ≠ 0) (h : ∃ (c : R), ofCoeff c = ofCoeff (powNat x n) / ofCoeff (powNat y (n - 1))) : powNat x n = powNat y (n - 1) * divExp x y n

A Brown scalar quotient in the embedding image satisfies the exact scale recurrence used by BrownLaw.