Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fact_zero_lt_one

Modification history

2023-01-11 07:28
src/geometry/manifold/instances/real.lean
feat(number_theory/bernoulli): Fourier coefficients of Bernoulli polynomials (#17990) …
Deleted fact_zero_lt_oneView on Github →
2021-03-24 16:04
src/geometry/manifold/instances/real.lean
feat(tactic/lint): linter for @[class] def (#6061) …
Modified fact_zero_lt_oneView on Github →
2020-07-25 15:23
src/geometry/manifold/real_instances.lean
chore(geometry/manifold/real_instance): remove global fact instance (#3549) …
Added fact_zero_lt_oneView on Github →