Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-01-29 17:00
4aa3eee4
View on Github →
chore(*): add inhabited instances (
#1898
)
chore(*): add inhabited instances
Fix linting errors.
Estimated changes
Modified
scripts/nolints.txt
Modified
src/algebra/associated.lean
Modified
src/algebra/category/CommRing/basic.lean
Modified
src/algebra/category/Group.lean
Modified
src/algebra/category/Mon/basic.lean
Modified
src/algebra/continued_fractions/basic.lean
added
def
continued_fraction.of_integer
added
def
generalized_continued_fraction.of_integer
added
def
simple_continued_fraction.of_integer
Modified
src/algebra/direct_sum.lean
Modified
src/algebra/free.lean
Modified
src/algebra/group/free_monoid.lean
deleted
theorem
free_add_monoid.add_def
deleted
theorem
free_add_monoid.zero_def
deleted
def
free_add_monoid
modified
theorem
free_monoid.mul_def
modified
theorem
free_monoid.one_def
Modified
src/algebra/group/hom.lean
Modified
src/algebra/group/to_additive.lean
Modified
src/algebra/group/type_tags.lean
Modified
src/algebra/group/units.lean
Modified
src/algebra/group/with_one.lean
Modified
src/algebra/module.lean
Modified
src/analysis/calculus/times_cont_diff.lean
Modified
src/analysis/complex/exponential.lean
Modified
src/analysis/normed_space/basic.lean
modified
structure
normed_group.core
Modified
src/category/fold.lean
Modified
src/category_theory/category/Groupoid.lean
Modified
src/category_theory/category/Rel.lean
Modified
src/category_theory/discrete_category.lean
Modified
src/computability/partrec_code.lean
Modified
src/computability/turing_machine.lean
Modified
src/data/buffer/basic.lean
Modified
src/data/dlist/instances.lean
Modified
src/data/equiv/algebra.lean
Modified
src/data/finmap.lean
Modified
src/data/fp/basic.lean
Modified
src/data/hash_map.lean
Modified
src/data/lazy_list2.lean
deleted
def
lazy_list.thunk.mk
added
def
thunk.mk
Modified
src/data/list/alist.lean
added
theorem
alist.ext_iff
Modified
src/data/matrix/basic.lean
Modified
src/data/mv_polynomial.lean
Modified
src/data/nat/enat.lean
Modified
src/data/nat/prime.lean
Modified
src/data/num/basic.lean
Modified
src/data/opposite.lean
Modified
src/data/padics/padic_integers.lean
Modified
src/data/padics/padic_numbers.lean
Modified
src/data/pfun.lean
Modified
src/data/pnat/basic.lean
Modified
src/data/pnat/factors.lean
Modified
src/data/pnat/xgcd.lean
Modified
src/data/polynomial.lean
Modified
src/data/quot.lean
Modified
src/data/real/cau_seq.lean
Modified
src/data/rel.lean
Modified
src/data/semiquot.lean
Modified
src/data/seq/computation.lean
Modified
src/data/seq/seq.lean
Modified
src/data/seq/wseq.lean
Modified
src/data/stream/basic.lean
Modified
src/data/tree.lean
Modified
src/data/zmod/basic.lean
Modified
src/data/zsqrtd/basic.lean
Modified
src/field_theory/mv_polynomial.lean
Modified
src/field_theory/perfect_closure.lean
Modified
src/group_theory/abelianization.lean
Modified
src/group_theory/congruence.lean
Modified
src/group_theory/free_abelian_group.lean
Modified
src/group_theory/free_group.lean
Modified
src/group_theory/monoid_localization.lean
Modified
src/group_theory/submonoid.lean
Modified
src/linear_algebra/basic.lean
Modified
src/linear_algebra/bilinear_form.lean
Modified
src/linear_algebra/dual.lean
Modified
src/linear_algebra/multilinear.lean
Modified
src/linear_algebra/sesquilinear_form.lean
Modified
src/linear_algebra/tensor_product.lean
Modified
src/logic/basic.lean
Modified
src/measure_theory/ae_eq_fun.lean
Modified
src/measure_theory/bochner_integration.lean
Modified
src/measure_theory/integration.lean
Modified
src/measure_theory/l1_space.lean
Modified
src/measure_theory/measurable_space.lean
Modified
src/meta/expr.lean
Modified
src/meta/rb_map.lean
Modified
src/order/bounded_lattice.lean
Modified
src/order/filter/basic.lean
Modified
src/order/filter/filter_product.lean
Modified
src/order/lexicographic.lean
Modified
src/order/pilex.lean
Modified
src/ring_theory/adjoin_root.lean
Modified
src/ring_theory/algebra.lean
Modified
src/ring_theory/free_comm_ring.lean
Modified
src/ring_theory/free_ring.lean
Modified
src/ring_theory/localization.lean
Modified
src/ring_theory/maps.lean
Modified
src/ring_theory/power_series.lean
Modified
src/set_theory/game.lean
Modified
src/set_theory/lists.lean
Modified
src/set_theory/ordinal.lean
Modified
src/set_theory/ordinal_notation.lean
Modified
src/set_theory/pgame.lean
Modified
src/set_theory/surreal.lean
Modified
src/set_theory/zfc.lean
added
def
arity.const
added
theorem
pSet.arity.equiv_const
Modified
src/tactic/abel.lean
Modified
src/tactic/core.lean
Created
src/tactic/derive_inhabited.lean
Modified
src/tactic/explode.lean
Modified
src/tactic/finish.lean
Modified
src/tactic/linarith.lean
Modified
src/tactic/lint.lean
Modified
src/tactic/monotonicity/basic.lean
Modified
src/tactic/monotonicity/interactive.lean
Modified
src/tactic/omega/eq_elim.lean
Modified
src/tactic/omega/find_ees.lean
Modified
src/tactic/omega/int/form.lean
Modified
src/tactic/omega/int/preterm.lean
Modified
src/tactic/omega/nat/form.lean
Modified
src/tactic/omega/nat/preterm.lean
Modified
src/tactic/omega/term.lean
Modified
src/tactic/rewrite_all/basic.lean
Modified
src/tactic/ring.lean
Modified
src/tactic/ring2.lean
Modified
src/tactic/ring_exp.lean
Modified
src/tactic/suggest.lean
Modified
src/tactic/tfae.lean
modified
inductive
tactic.tfae.arrow
Modified
src/topology/algebra/module.lean
Modified
src/topology/compact_open.lean
Modified
src/topology/metric_space/gluing.lean
Modified
src/topology/metric_space/gromov_hausdorff.lean
Modified
src/topology/opens.lean
Modified
src/topology/stone_cech.lean
Modified
src/topology/subset_properties.lean
Modified
src/topology/uniform_space/basic.lean
Modified
src/topology/uniform_space/compare_reals.lean
modified
def
compare_reals.Q
Modified
src/topology/uniform_space/completion.lean
Modified
src/topology/uniform_space/separation.lean