Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-11 12:23 7fd7ea8c

View on Github →

fix(analysis/real): more irreducible

Estimated changes

Modified algebra/linear_algebra/prod_module.lean

Modified analysis/ennreal.lean

Modified analysis/real.lean

added theorem max_of_rat

deleted theorem max_of_rat_of_rat

added theorem min_of_rat

deleted theorem min_of_rat_of_rat

added theorem of_rat_le

deleted theorem of_rat_le_of_rat

added theorem real.le_def

modified theorem two_eq_of_rat_two