Theorem Rat.cast_def

Modification history

2024-04-06 09:41

Mathlib/Algebra/Field/Defs.lean

refactor: Avoid `Rat` internals in the definition of `Field` (#11639) …

Modified Rat.cast_def View on Github →

2022-11-30 21:35

Mathlib/Algebra/Field/Defs.lean

feat: port Algebra.Field.Defs (#668) …

Added Rat.cast_def View on Github →