leanprover-community/mathlib

Pull Requests Commits

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

vihdzp committed 3 years ago

a3c647bb

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

dtumad committed 3 years ago

f0f40704

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

urkud committed 3 years ago

8927a02c

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

eric-wieser committed 3 years ago

0e3184fc

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

alreadydone committed 3 years ago

2a7ceb0e

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

YaelDillies committed 3 years ago

a5a6865f

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

isadofschi committed 3 years ago

70a27086

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

pechersky committed 3 years ago

646028a0

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

urkud committed 3 years ago

8a80759b

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

Vierkantor committed 3 years ago

b4979cbd

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

urkud committed 3 years ago

7428bd9b

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

vihdzp committed 3 years ago

691f04fe

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

pechersky committed 3 years ago

6df59d68

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

kmill committed 3 years ago

58525685

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

vihdzp committed 3 years ago

1422d387

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

alexjbest committed 3 years ago

0d186304

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

vihdzp committed 3 years ago

bf735cd1

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

eric-wieser committed 3 years ago

9b2755b9

chore(data/nat): rename oddly named lemma odd_gt_zero (#13040)

alexjbest committed 3 years ago

ab99fd1b

feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136)

apnelson1 committed 3 years ago

6d02dac3

feat(combinatorics/simple_graph/basic): `dart.to_prod` is injective (#15150)

kmill committed 3 years ago

418373e8

feat(data/quot): `is_equiv` instance for quotient equivalence (#15148)

vihdzp committed 3 years ago

3e52000c

feat(order/rel_iso): add `rel_iso.cast` (#15144)

vihdzp committed 3 years ago

e034eb09

refactor(group_theory/congruence): use `quotient.map` (#15130)

urkud committed 3 years ago

e335a41f

feat(measure_theory/integral): Circle integral transform (#13885)

CBirkbeck committed 3 years ago

fdfc2229

chore(set_theory/ordinal/basic): clean up `ordinal.card` API (#15147)

vihdzp committed 3 years ago

0a89f18f

feat(set_theory/ordinal/basic): basic lemmas on `ordinal.lift` (#15146)

vihdzp committed 3 years ago

a54e63da

feat(order/basic): a symmetric relation implies equality when it implies less-equal (#15149)

vihdzp committed 3 years ago

b7581040

refactor(topology/separation): redefine `t0_space` (#15046)

urkud committed 3 years ago

d45a8ace

feat(analysis/inner_product_space): add simple lemmas for the orthogonal complement (#15020)

mcdoll committed 3 years ago

71b1be63

Newer Older