Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-08 14:30 3aeb64ca

View on Github →

refactor(*): touching up proofs from 'faster' branch

Estimated changes

Modified algebra/big_operators.lean

Modified algebra/euclidean_domain.lean

Modified algebra/field.lean

deleted theorem inv_sub_inv_eq

Modified algebra/gcd_domain.lean

modified theorem dvd_lcm_left

modified theorem dvd_lcm_right

modified theorem lcm_dvd_iff

Modified algebra/group_power.lean

modified theorem neg_one_pow_eq_or

Modified algebra/ordered_group.lean

added theorem add_eq_zero_iff'

deleted theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'

Modified analysis/topology/topological_space.lean

Modified data/finset.lean

modified theorem finset.card_insert_of_not_mem

modified theorem finset.coe_empty

modified theorem finset.coe_singleton

modified theorem finset.fold_singleton

modified theorem finset.max_singleton'

modified theorem finset.max_singleton

modified theorem finset.mem_singleton

modified theorem finset.min_empty

modified theorem finset.min_singleton

modified theorem list.to_finset_card_of_nodup

Modified data/finsupp.lean

modified theorem finsupp.mem_support_iff

added theorem finsupp.not_mem_support_iff

modified theorem finsupp.single_apply

modified theorem finsupp.single_eq_of_ne

modified theorem finsupp.single_eq_same

Modified data/list/basic.lean

modified theorem list.count_singleton

modified theorem list.forall_mem_nil

modified theorem list.join_eq_nil

modified theorem list.not_exists_mem_nil

modified theorem list.take_zero

modified theorem option.to_list_nodup

Modified data/nat/basic.lean

added theorem nat.succ_inj'

Modified data/polynomial.lean

modified theorem polynomial.nat_degree_zero

Modified data/set/lattice.lean

added theorem set.sInter_pair

added theorem set.sUnion_pair

Modified order/basic.lean

Modified order/conditionally_complete_lattice.lean

modified theorem bdd_above_finite

modified theorem bdd_above_subset

modified theorem bdd_below_subset

Modified order/filter.lean

Modified set_theory/ordinal.lean