mathlib3

126cebca - feat(data/real/nnreal): ℝ is an ℝ≥0-algebra (#6560)

feat(data/real/nnreal): ℝ is an ℝ≥0-algebra (#6560) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype