Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 22:35 720fa8fa

View on Github →

feat(data/rat/basic): API around rat.mk (#10782)

Estimated changes

Modified src/data/rat/basic.lean

added theorem rat.denom_mk

added theorem rat.ext

added theorem rat.ext_iff

added theorem rat.mk_neg_denom

added theorem rat.num_mk

Modified src/number_theory/bernoulli.lean

Modified src/number_theory/number_field.lean