Commits leanprover-community/mathlib

feat(data/rat/defs): add denominator as pnat (#15101)

Jon Eugster committed 4 years ago

11cdccb8

chore(data/nat/squarefree): fix a tactic doc typo for norm num extension (#15189)

alexjbest committed 4 years ago

feb34df6

fix(data/fintype/basic): move card_subtype_mono into the fintype namespace (#15185)

wrenna-robson committed 4 years ago

5a5d2909

feat(analysis/normed_space/lp_space): normed_algebra structure (#15086)

eric-wieser committed 4 years ago

1937dff0

doc(tactic/wlog): use markdown lists rather than indentation (#15113)

eric-wieser committed 4 years ago

e74e5349

feat(topology/metric_space/hausdorff_distance): Thickening a compact inside an open (#14926)

YaelDillies committed 4 years ago

0bc51f02

feat(combinatorics/simple_graph/prod): Box product (#14867)

YaelDillies committed 4 years ago

93be74b1

feat(data/finset/basic): Coercion of a product of finsets (#15011)

YaelDillies committed 4 years ago

7c070c4d

feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970)

eric-wieser committed 4 years ago

d34b3306

chore(topology/algebra/semigroup): golf file (#14957)

vihdzp committed 4 years ago

563a51af

feat(topology/algebra/uniform_group): `uniform_group` is preserved by Inf and comap (#14889)

ADedecker committed 4 years ago

ba9f346a

refactor(set_theory/cardinal/basic): migrate from `fintype` to `finite` (#15175)

urkud committed 4 years ago

6eeb941c

feat(set_theory/ordinal/arithmetic): tweak theorems about `0` and `1` (#15174)

vihdzp committed 4 years ago

a3c647bb

feat(topology/algebra/infinite_sum): Double sum is equal to a single value (#15157)

dtumad committed 4 years ago

f0f40704

chore(tactic/lift): move a proof to `subtype.exists_pi_extension` (#15098)

urkud committed 4 years ago

8927a02c

feat(data/fin/tuple/basic): add lemmas for rewriting exists and forall over `n+1`-tuples (#15048)

eric-wieser committed 4 years ago

0e3184fc

perf(linear_algebra): speed up `graded_algebra` instances (#14967)

alreadydone committed 4 years ago

2a7ceb0e

feat(combinatorics/set_family/intersecting): Intersecting families (#14475)

YaelDillies committed 4 years ago

a5a6865f

feat(topology/continuous_function): Any T0 space embeds in a product of copies of the Sierpinski space (#14036)

isadofschi committed 4 years ago

70a27086

refactor(data/finset/lattice): finset.{min,max} away from option (#15163)

pechersky committed 4 years ago

646028a0

feat(order/filter/basic): add `map_le_map` and `map_injective` (#15128)

urkud committed 4 years ago

8a80759b

chore(data/rat): split `field ℚ` instance from definition of `ℚ` (#14893)

Vierkantor committed 4 years ago

b4979cbd

refactor(data/finite/set,data/set/finite): move most contents of one file to another (#15166)

urkud committed 4 years ago

7428bd9b

feat(order/rel_iso): two reflexive/irreflexive relations on a unique type are isomorphic (#14760)

vihdzp committed 4 years ago

691f04fe

feat(data/list/basic): nth_le_enum (#15139)

pechersky committed 4 years ago

6df59d68

feat(combinatorics/simple_graph/{basic,subgraph,clique,coloring}): add induced graphs, characterization of cliques, and bounds for colorings (#14034)

kmill committed 4 years ago

58525685

feat(order/succ_pred): expand API on `with_bot` and `with_top` (#15016)

vihdzp committed 4 years ago

1422d387

chore(ring_theory/norm): generalise a couple of lemmas (#15160)

alexjbest committed 4 years ago

0d186304

chore(set_theory/ordinal/basic): remove `rel_iso_out` (#15145)

vihdzp committed 4 years ago

bf735cd1

chore(*): add missing `to_fun → apply` configurations for `simps` (#15112)

eric-wieser committed 4 years ago

9b2755b9