Theory real_algebra

⊢ Reals =
  <|carrier := 𝕌(:real); sum := real_add_monoid; prod := real_mul_monoid|>

⊢ real_add_monoid = <|carrier := 𝕌(:real); id := 0; op := $+ |>

⊢ real_mul_monoid = <|carrier := 𝕌(:real); id := 1; op := $* |>

⊢ ∀f s.
    FINITE s ⇒ GBAG Reals.prod (BAG_IMAGE f (BAG_OF_SET s)) = product s f

⊢ ∀f s. FINITE s ⇒ GBAG Reals.sum (BAG_IMAGE f (BAG_OF_SET s)) = SIGMA f s

⊢ r ≠ 0 ⇒ Inv Reals r = r⁻¹

⊢ Reals.sum.inv = numeric_negate

⊢ Ring Reals

⊢ Unit Reals r ⇔ r ≠ 0

⊢ AbelianGroup real_add_monoid

⊢ AbelianMonoid real_add_monoid

⊢ real_add_monoid.carrier = 𝕌(:real) ∧ real_add_monoid.op = $+ ∧
  real_add_monoid.id = 0

⊢ AbelianGroup (real_mul_monoid excluding 0)

⊢ AbelianMonoid real_mul_monoid

⊢ real_mul_monoid.carrier = 𝕌(:real) ∧ real_mul_monoid.op = $* ∧
  real_mul_monoid.id = 1

⊢ ring_divides Reals p q ⇔ p = 0 ⇒ q = 0

⊢ ring_prime Reals p