Mathlib v3 is deprecated. Go to Mathlib v4

Def algebra.semiring_to_ring

Modification history

2021-11-17 07:06
src/algebra/algebra/basic.lean
lint(*): curly braces linter (#10280) …
Modified algebra.semiring_to_ringView on Github →
2020-09-26 15:49
src/ring_theory/algebra.lean
feat(ring_theory/algebra, algebra/module): Add add_comm_monoid_to_add_comm_group and semiring_to_ring (#4252)
Added algebra.semiring_to_ringView on Github →