leanprover-community/mathlib

Pull Requests Commits

urkud committed 4 years ago

4e95f7c1

chore(order/complete_lattice): golf a few proofs

urkud committed 4 years ago

ee7cef51

feat(topology/bases): a family of nonempty disjoint open sets is countable in a separable space (#9557)

sgouezel committed 4 years ago

fdf8a71f

feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are (#9538)

ocfnash committed 4 years ago

815eaca0

doc(linear_algebra/free_module/strong_rank_condition): correct a typo (#9565)

riccardobrasca committed 4 years ago

63903f27

feat(order/bounds): Image under an `order_iso` and `upper_bounds` commute (#9555)

YaelDillies committed 4 years ago

0b575206

feat(data/int/interval): Finite intervals in ℤ (#9526)

YaelDillies committed 4 years ago

111d73bf

chore(linear_algebra/quadratic_form): speed up quadratic_form.lin_mul_lin (#9567)

Ruben-VandeVelde committed 4 years ago

7455f47c

fix(data/equiv/basic): use `subtype p` not `coe_sort (set_of p)` (#9559)

eric-wieser committed 4 years ago

5926f103

chore(measure_theory/*): better names and notations, add easy lemmas (#9554)

sgouezel committed 4 years ago

da4d5501

feat(analysis/convex/basic): Levels of a monotone/antitone function (#9547)

YaelDillies committed 4 years ago

e7ea02fd

feat(ring_theory/polynomial/basic): add a lemma `polynomial_quotient_equiv_quotient_polynomial_map_mk` (#9542)

Paul-Lez committed 4 years ago

5b793197

refactor(algebra/gcd_monoid): don't require normalization (#9443)

Ruben-VandeVelde committed 4 years ago

26660331

refactor(topology/algebra/module): continuous semilinear maps (#9539)

dupuisf committed 4 years ago

def4814c

refactor(analysis/convex/*): prove `convex_independent_iff_finset` without full Carathéodory (#9550)

YaelDillies committed 4 years ago

fefd8a38

feat(topology/algebra): adic topology (#9521)

PatrickMassot committed 4 years ago

c42786f5

ci(.github/workflows): automatically remove awaiting-CI label (#9491)

bryangingechen committed 4 years ago

61cd266a

refactor(data/polynomial): use `monic.ne_zero` and `nontriviality` (#9530)

Vierkantor committed 4 years ago

15364121

chore(scripts): update nolints.txt (#9553)

leanprover-community-bot committed 4 years ago

fd189536

docs(ring_theory/adjoin_root): fix docstring (#9546)

jcommelin committed 4 years ago

04916217

feat(number_theory/padics): add padic_norm lemmas (#9527)

mariainesdff committed 4 years ago

74664245

fix(order/sub): make arguments explicit (#9541)

fpvandoorn committed 4 years ago

3aac8e5f

feat(set_theory/cardinal,*): assorted lemmas (#9516)

urkud committed 4 years ago

10da8e67

refactor(group_theory/is_p_group): Generalize `is_p_group.comap_injective` (#9509)

tb65536 committed 4 years ago

50b51c5e

feat(data/pnat/interval): Finite intervals in ℕ+ (#9534)

YaelDillies committed 4 years ago

7a5d15a9

feat(order/conditionally_complete_lattice): image and cSup commute (#9510)

YaelDillies committed 4 years ago

e998e4c4

feat(algebra/order/functions): recursors and images under monotone maps (#9505)

YaelDillies committed 4 years ago

d8968ba7

refactor(order/fixed_points): rewrite using bundled `preorder_hom`s (#9497)

urkud committed 4 years ago

fa520678

feat(topology/homotopy): add `homotopy_with` (#9252)

shingtaklam1324 committed 4 years ago

387ff6e3

fix(ci): always use python3 executable (#9531)

gebner committed 4 years ago

f6c77be6

Older