Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-02-04 02:33
4cfc30e3
View on Github →
chore(*): use le_rfl instead of le_refl _ (
#11797
)
Estimated changes
Modified
src/algebra/algebra/operations.lean
Modified
src/algebra/algebra/subalgebra.lean
Modified
src/algebra/big_operators/order.lean
Modified
src/algebra/direct_limit.lean
Modified
src/algebra/indicator_function.lean
Modified
src/algebra/lie/nilpotent.lean
Modified
src/algebra/lie/submodule.lean
Modified
src/algebra/order/archimedean.lean
Modified
src/algebra/order/monoid.lean
Modified
src/algebra/order/pi.lean
Modified
src/algebra/order/ring.lean
Modified
src/algebra/order/with_zero.lean
Modified
src/algebra/tropical/basic.lean
Modified
src/algebraic_topology/simplex_category.lean
Modified
src/analysis/analytic/basic.lean
Modified
src/analysis/asymptotics/asymptotics.lean
Modified
src/analysis/calculus/deriv.lean
Modified
src/analysis/calculus/fderiv.lean
Modified
src/analysis/calculus/fderiv_measurable.lean
Modified
src/analysis/calculus/fderiv_symmetric.lean
Modified
src/analysis/calculus/inverse.lean
Modified
src/analysis/calculus/times_cont_diff.lean
Modified
src/analysis/inner_product_space/projection.lean
Modified
src/analysis/normed/group/SemiNormedGroup/kernels.lean
Modified
src/analysis/normed/group/basic.lean
Modified
src/analysis/normed/group/infinite_sum.lean
Modified
src/analysis/normed/group/quotient.lean
Modified
src/analysis/normed_space/basic.lean
Modified
src/analysis/normed_space/enorm.lean
Modified
src/analysis/normed_space/multilinear.lean
Modified
src/analysis/special_functions/bernstein.lean
Modified
src/analysis/specific_limits.lean
Modified
src/category_theory/sites/closed.lean
Modified
src/category_theory/sites/grothendieck.lean
Modified
src/category_theory/sites/pretopology.lean
Modified
src/category_theory/subobject/basic.lean
Modified
src/combinatorics/composition.lean
Modified
src/computability/language.lean
Modified
src/computability/partrec_code.lean
Modified
src/computability/turing_machine.lean
Modified
src/control/lawful_fix.lean
Modified
src/data/W/basic.lean
Modified
src/data/W/cardinal.lean
Modified
src/data/analysis/filter.lean
Modified
src/data/buffer/parser/basic.lean
Modified
src/data/complex/exponential.lean
Modified
src/data/finset/lattice.lean
Modified
src/data/fintype/basic.lean
Modified
src/data/int/basic.lean
Modified
src/data/list/min_max.lean
Modified
src/data/list/rotate.lean
Modified
src/data/multiset/finset_ops.lean
Modified
src/data/multiset/lattice.lean
Modified
src/data/mv_polynomial/cardinal.lean
Modified
src/data/mv_polynomial/variables.lean
Modified
src/data/nat/basic.lean
Modified
src/data/nat/cast.lean
Modified
src/data/nat/choose/basic.lean
Modified
src/data/nat/enat.lean
Modified
src/data/nat/factorial/basic.lean
Modified
src/data/nat/lattice.lean
Modified
src/data/nat/pow.lean
Modified
src/data/nat/prime.lean
Modified
src/data/ordmap/ordnode.lean
Modified
src/data/ordmap/ordset.lean
Modified
src/data/polynomial/degree/definitions.lean
Modified
src/data/polynomial/degree/trailing_degree.lean
Modified
src/data/polynomial/eval.lean
Modified
src/data/polynomial/field_division.lean
Modified
src/data/polynomial/inductions.lean
Modified
src/data/polynomial/reverse.lean
Modified
src/data/rbtree/basic.lean
Modified
src/data/real/basic.lean
Modified
src/data/real/cau_seq.lean
Modified
src/data/real/ennreal.lean
Modified
src/data/real/ereal.lean
Modified
src/data/real/pi/bounds.lean
Modified
src/data/real/pi/wallis.lean
Modified
src/data/real/sqrt.lean
Modified
src/data/set/intervals/disjoint.lean
Modified
src/field_theory/adjoin.lean
Modified
src/field_theory/galois.lean
Modified
src/field_theory/is_alg_closed/basic.lean
Modified
src/field_theory/splitting_field.lean
Modified
src/geometry/manifold/instances/real.lean
Modified
src/geometry/manifold/times_cont_mdiff.lean
Modified
src/group_theory/perm/support.lean
Modified
src/group_theory/specific_groups/alternating.lean
Modified
src/group_theory/subgroup/basic.lean
Modified
src/linear_algebra/adic_completion.lean
Modified
src/linear_algebra/basic.lean
Modified
src/linear_algebra/bilinear_form.lean
Modified
src/linear_algebra/dimension.lean
Modified
src/linear_algebra/finite_dimensional.lean
Modified
src/linear_algebra/isomorphisms.lean
Modified
src/linear_algebra/linear_independent.lean
Modified
src/linear_algebra/quotient.lean
Modified
src/linear_algebra/std_basis.lean
Modified
src/measure_theory/decomposition/lebesgue.lean
Modified
src/measure_theory/decomposition/unsigned_hahn.lean
Modified
src/measure_theory/function/l1_space.lean
Modified
src/measure_theory/function/lp_space.lean
Modified
src/measure_theory/integral/integrable_on.lean
Modified
src/measure_theory/integral/integral_eq_improper.lean
Modified
src/measure_theory/integral/interval_integral.lean
Modified
src/measure_theory/integral/lebesgue.lean
Modified
src/measure_theory/integral/vitali_caratheodory.lean
Modified
src/measure_theory/measurable_space_def.lean
Modified
src/measure_theory/measure/giry_monad.lean
Modified
src/measure_theory/measure/measure_space.lean
Modified
src/measure_theory/measure/outer_measure.lean
Modified
src/measure_theory/measure/stieltjes.lean
Modified
src/measure_theory/measure/vector_measure.lean
Modified
src/measure_theory/pi_system.lean
Modified
src/number_theory/class_number/finite.lean
Modified
src/number_theory/padics/hensel.lean
Modified
src/number_theory/padics/padic_numbers.lean
Modified
src/number_theory/primorial.lean
Modified
src/number_theory/quadratic_reciprocity.lean
Modified
src/number_theory/sum_four_squares.lean
Modified
src/number_theory/zsqrtd/basic.lean
Modified
src/order/atoms.lean
Modified
src/order/bounded_order.lean
Modified
src/order/closure.lean
Modified
src/order/complete_lattice.lean
Modified
src/order/conditionally_complete_lattice.lean
Modified
src/order/filter/at_top_bot.lean
Modified
src/order/filter/bases.lean
Modified
src/order/filter/extr.lean
Modified
src/order/filter/indicator_function.lean
Modified
src/order/filter/lift.lean
Modified
src/order/filter/ultrafilter.lean
Modified
src/order/galois_connection.lean
Modified
src/order/lattice.lean
Modified
src/order/liminf_limsup.lean
Modified
src/order/modular_lattice.lean
Modified
src/order/monotone.lean
Modified
src/order/omega_complete_partial_order.lean
Modified
src/order/partial_sups.lean
Modified
src/order/pilex.lean
Modified
src/order/well_founded_set.lean
Modified
src/order/zorn.lean
Modified
src/probability_theory/stopping.lean
Modified
src/ring_theory/artinian.lean
Modified
src/ring_theory/dedekind_domain.lean
Modified
src/ring_theory/ideal/operations.lean
Modified
src/ring_theory/int/basic.lean
Modified
src/ring_theory/localization.lean
Modified
src/ring_theory/nakayama.lean
Modified
src/ring_theory/polynomial/basic.lean
Modified
src/ring_theory/polynomial/bernstein.lean
Modified
src/ring_theory/power_series/basic.lean
Modified
src/ring_theory/unique_factorization_domain.lean
Modified
src/ring_theory/valuation/basic.lean
modified
theorem
add_valuation.supp_quot_supp
modified
theorem
valuation.supp_quot_supp
Modified
src/set_theory/cardinal.lean
Modified
src/set_theory/cardinal_ordinal.lean
Modified
src/set_theory/cofinality.lean
Modified
src/set_theory/ordinal.lean
Modified
src/set_theory/ordinal_arithmetic.lean
Modified
src/testing/slim_check/sampleable.lean
Modified
src/topology/algebra/floor_ring.lean
Modified
src/topology/algebra/group.lean
Modified
src/topology/algebra/infinite_sum.lean
Modified
src/topology/algebra/ordered/intermediate_value.lean
Modified
src/topology/algebra/ordered/monotone_convergence.lean
Modified
src/topology/category/Top/open_nhds.lean
Modified
src/topology/continuous_function/bounded.lean
Modified
src/topology/instances/ennreal.lean
Modified
src/topology/list.lean
Modified
src/topology/local_extr.lean
Modified
src/topology/metric_space/baire.lean
Modified
src/topology/metric_space/basic.lean
Modified
src/topology/metric_space/contracting.lean
Modified
src/topology/metric_space/emetric_space.lean
Modified
src/topology/metric_space/gluing.lean
Modified
src/topology/metric_space/gromov_hausdorff.lean
Modified
src/topology/metric_space/gromov_hausdorff_realized.lean
Modified
src/topology/metric_space/lipschitz.lean
Modified
src/topology/order.lean
Modified
src/topology/path_connected.lean
Modified
src/topology/semicontinuous.lean
Modified
src/topology/separation.lean
Modified
src/topology/sheaves/sheaf_condition/equalizer_products.lean
Modified
src/topology/sheaves/sheaf_condition/opens_le_cover.lean
Modified
src/topology/stone_cech.lean
Modified
src/topology/uniform_space/basic.lean
Modified
src/topology/uniform_space/completion.lean
Modified
src/topology/uniform_space/separation.lean
Modified
src/topology/vector_bundle.lean
Modified
test/apply.lean
Modified
test/monotonicity.lean