@[reducible, inline]

abbrev Lean.Grind.Field.NormNum.ofRat {α : Type u_1} [Field α] (r : Rat) : α

Equations

• Lean.Grind.Field.NormNum.ofRat r = ↑r.num / ↑r.den

theorem Lean.Grind.Field.NormNum.ofRat_add' {α : Type u_1} [Field α] {a b : Rat} (ha : ↑a.den ≠ 0) (hb : ↑b.den ≠ 0) : ofRat (a + b) = ofRat a + ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_mul' {α : Type u_1} [Field α] {a b : Rat} (ha : ↑a.den ≠ 0) (hb : ↑b.den ≠ 0) : ofRat (a * b) = ofRat a * ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_add {α : Type u_1} [Field α] [IsCharP α 0] (a b : Rat) : ofRat (a + b) = ofRat a + ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_mul {α : Type u_1} [Field α] [IsCharP α 0] (a b : Rat) : ofRat (a * b) = ofRat a * ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_inv {α : Type u_1} [Field α] (a : Rat) : ofRat a⁻¹ = (ofRat a)⁻¹

theorem Lean.Grind.Field.NormNum.ofRat_div' {α : Type u_1} [Field α] {a b : Rat} (ha : ↑a.den ≠ 0) (hb : ↑b.num ≠ 0) : ofRat (a / b) = ofRat a / ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_div {α : Type u_1} [Field α] [IsCharP α 0] (a b : Rat) : ofRat (a / b) = ofRat a / ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_neg {α : Type u_1} [Field α] (a : Rat) : ofRat (-a) = -ofRat a

theorem Lean.Grind.Field.NormNum.ofRat_sub' {α : Type u_1} [Field α] {a b : Rat} (ha : ↑a.den ≠ 0) (hb : ↑b.den ≠ 0) : ofRat (a - b) = ofRat a - ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_sub {α : Type u_1} [Field α] [IsCharP α 0] (a b : Rat) : ofRat (a - b) = ofRat a - ofRat b

theorem Lean.Grind.Field.NormNum.ofRat_npow' {α : Type u_1} [Field α] {a : Rat} (ha : ↑a.den ≠ 0) (n : Nat) : ofRat (a ^ n) = ofRat a ^ n

theorem Lean.Grind.Field.NormNum.ofRat_npow {α : Type u_1} [Field α] [IsCharP α 0] (a : Rat) (n : Nat) : ofRat (a ^ n) = ofRat a ^ n

theorem Lean.Grind.Field.NormNum.ofRat_zpow' {α : Type u_1} [Field α] {a : Rat} (ha : ↑a.den ≠ 0) (n : Int) : ofRat (a ^ n) = ofRat a ^ n

theorem Lean.Grind.Field.NormNum.ofRat_zpow {α : Type u_1} [Field α] [IsCharP α 0] (a : Rat) (n : Int) : ofRat (a ^ n) = ofRat a ^ n

theorem Lean.Grind.Field.NormNum.natCast_eq {α : Type u_1} [Field α] (n : Nat) : ↑n = ofRat ↑n

theorem Lean.Grind.Field.NormNum.ofNat_eq {α : Type u_1} [Field α] (n : Nat) : OfNat.ofNat n = ofRat ↑n

theorem Lean.Grind.Field.NormNum.intCast_eq {α : Type u_1} [Field α] (n : Int) : IntCast.intCast n = ofRat ↑n

theorem Lean.Grind.Field.NormNum.add_eq {α : Type u_1} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat) : (v == v₁ + v₂) = true → a = ofRat v₁ → b = ofRat v₂ → a + b = ofRat v

theorem Lean.Grind.Field.NormNum.sub_eq {α : Type u_1} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat) : (v == v₁ - v₂) = true → a = ofRat v₁ → b = ofRat v₂ → a - b = ofRat v

theorem Lean.Grind.Field.NormNum.mul_eq {α : Type u_1} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat) : (v == v₁ * v₂) = true → a = ofRat v₁ → b = ofRat v₂ → a * b = ofRat v

theorem Lean.Grind.Field.NormNum.div_eq {α : Type u_1} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat) : (v == v₁ / v₂) = true → a = ofRat v₁ → b = ofRat v₂ → a / b = ofRat v

theorem Lean.Grind.Field.NormNum.inv_eq {α : Type u_1} [Field α] (a : α) (v₁ v : Rat) : (v == v₁⁻¹) = true → a = ofRat v₁ → a⁻¹ = ofRat v

theorem Lean.Grind.Field.NormNum.neg_eq {α : Type u_1} [Field α] (a : α) (v₁ v : Rat) : (v == -v₁) = true → a = ofRat v₁ → -a = ofRat v

theorem Lean.Grind.Field.NormNum.npow_eq {α : Type u_1} [Field α] [IsCharP α 0] (a : α) (n : Nat) (v₁ v : Rat) : (v == v₁ ^ n) = true → a = ofRat v₁ → a ^ n = ofRat v

theorem Lean.Grind.Field.NormNum.zpow_eq {α : Type u_1} [Field α] [IsCharP α 0] (a : α) (n : Int) (v₁ v : Rat) : (v == v₁ ^ n) = true → a = ofRat v₁ → a ^ n = ofRat v

theorem Lean.Grind.Field.NormNum.eq_int {α : Type u_1} [Field α] (a : α) (v : Rat) (n : Int) : (n == v.num && v.den == 1) = true → a = ofRat v → a = IntCast.intCast n

theorem Lean.Grind.Field.NormNum.eq_inv {α : Type u_1} [Field α] (a : α) (v : Rat) (d : Nat) : (v.num == 1 && v.den == d) = true → a = ofRat v → a = (↑d)⁻¹

theorem Lean.Grind.Field.NormNum.eq_mul_inv {α : Type u_1} [Field α] (a : α) (v : Rat) (n : Int) (d : Nat) : (v.num == n && v.den == d) = true → a = ofRat v → a = IntCast.intCast n * (↑d)⁻¹