leanprover-community/mathlib3

Pull Requests Commits

subtheory_model

awainverse committed 3 years ago

09971712

move_subtheory_model

awainverse committed 3 years ago

ec322701

Revert "is_maximal"

awainverse committed 3 years ago

ef112cc6

Revert "Revert "init""

awainverse committed 3 years ago

a90c2b16

awainverse committed 3 years ago

3237e0b5

awainverse committed 3 years ago

d4d5c814

feat(topology): is_open and is_closed in term of ∀ᶠ and ∃ᶠ (#16545)

PatrickMassot committed 3 years ago

b4502fd1

awainverse committed 3 years ago

973725df

feat(probability/martingale/borel_cantelli): Lévy's generalized Borel-Cantelli (#16358)

kex-y committed 3 years ago

8c9342fd

feat(archive/birthday): improve birthday problem (#16528)

ericrbg committed 3 years ago

827a83eb

doc(number_theory/legendre_symbol/jacobi_symbol): remove now spurious reference to 'subscript J' (#16541)

MichaelStollBayreuth committed 3 years ago

7e74869c

feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514)

mcdoll committed 3 years ago

1dc531a0

chore(topology/constructions): deduplicate (#16505)

urkud committed 3 years ago

ba584a4c

chore(algebra/order/nonneg): add a `distrib_lattice` instance (#16493)

eric-wieser committed 3 years ago

f8dfe810

chore(order/symm_diff): Generalize to co-Heyting algebras (#16282)

YaelDillies committed 3 years ago

57bbd9ec

feat(topology/separation): define `T₅` spaces (#16533)

urkud committed 3 years ago

f7e477fd

doc(order/filter/basic): fix notations in doc of filter.comap (#16530)

xroblot committed 3 years ago

0ff46b9c

move(algebra/field_power): Put lemmas in the correct place (#16465)

YaelDillies committed 3 years ago

a4f6c41e

docs(data/list/defs): fix `list.dedup` docstring (#16535)

kmill committed 3 years ago

86a14674

feat(number_theory): Dedekind-Kummer theorem (#15000)

Vierkantor committed 3 years ago

1e225257

chore(algebra/order/monoid_lemmas_zero_lt): remove redundant assumptions (#16524)

astrainfinita committed 3 years ago

e763499b

doc(category/abelian/ext): update module doc (#16512)

kim-em committed 3 years ago

7a9e6ca4

feat(number_theory/legendre_symbol/norm_num): add file with `norm_num` extension for the Jacobi symbol (#16519)

MichaelStollBayreuth committed 3 years ago

8922aaa5

refactor(number_theory/padics/padic_val): make prime implicit (#15221)

Multramate committed 3 years ago

894c8c22

feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors (#16153)

eric-wieser committed 3 years ago

d46774d4

feat(archive/100-theorems-list): Stirling, part 2 (#14875)

mo271 committed 3 years ago

fc35e1e9

feat(combinatorics/simple_graph/prod): add `locally_finite` instance for the box product of `locally_finite` graphs, plus two related lemmas (#16431)

bottine committed 3 years ago

104f141e

feat(linear_algebra/symplectic_group): add definition of symplectic group (#15513)

mpenciak committed 3 years ago

a5b382d8

fix(tactic/monotonicity/interactive): fix the order of calling `unify_with_instance` (#16480)

astrainfinita committed 3 years ago

69be6fe3

feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ (#16488)

j-loreaux committed 3 years ago

f1397dc1

Newer Older