Commit 2023-09-05 09:13 6aa77b12

View on Github →

chore: split out IsField (#6954)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Field/Defs.lean

deleted theorem Field.toIsField

deleted theorem IsField.nontrivial

deleted structure IsField

deleted theorem Semifield.toIsField

deleted theorem not_isField_of_subsingleton

deleted theorem uniq_inv_of_isField

Created Mathlib/Algebra/Field/IsField.lean

added theorem Field.toIsField

added theorem IsField.nontrivial

added structure IsField

added theorem Semifield.toIsField

added theorem not_isField_of_subsingleton

added theorem uniq_inv_of_isField

Modified Mathlib/Algebra/Ring/Equiv.lean