Commit 2023-08-14 12:56 1e78d106

View on Github →

feat: Minimal axioms for rings and fields (#6472)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Field/MinimalAxioms.lean

added def Field.ofMinimalAxioms

Created Mathlib/Algebra/Ring/MinimalAxioms.lean

added def CommRing.ofMinimalAxioms

added def Ring.ofMinimalAxioms