Commit 2022-11-30 21:35 d0c22ca9

View on Github →

feat: port Algebra.Field.Defs (#668) Tracking mathlib commit: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

added theorem Field.toIsField
added theorem IsField.nontrivial
added structure IsField
added def Rat.castRec
added theorem Rat.cast_def
added theorem Rat.cast_mk'
added theorem Rat.smul_def
added theorem Semifield.toIsField
added def qsmulRec
added theorem uniq_inv_of_is_field