leanprover-community/mathlib

Pull Requests Commits

docs(algebra/module/equiv): correct a misleading comment (#18458)

eric-wieser committed 3 years ago

ea94d7cd

refactor(topology/metric_space): drop `dist_setoid` (#18502)

urkud committed 3 years ago

0c1f285a

feat(matrix/dual_number): `matrix` and `dual_number` commute (#18386)

eric-wieser committed 3 years ago

eb0cb451

chore(number_theory/pell*): rename files, update doc (#18503)

MichaelStollBayreuth committed 3 years ago

a66d07e2

feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)

vihdzp committed 3 years ago

c6b53304

fix (measure_theory/measure/measure_space_def): fix module docstring typos (#18500)

kbuzzard committed 3 years ago

146a2eed

docs(set_theory/lists): update docs (#18346)

astrainfinita committed 3 years ago

497d1e06

chore(data/finset/lattice): Protect a few more lemmas (#18497)

YaelDillies committed 3 years ago

1c857a1f

feat(data/polynomial/div): prove that evaluation induces an isomorphism of algebras (#18480)

Multramate committed 3 years ago

e064a7bf

feat(number_theory/pell_general): add general existence result for Pell's Equation (#18484)

MichaelStollBayreuth committed 3 years ago

c23aca35

feat(analysis/fourier): Poisson summation (#18392)

loefflerd committed 3 years ago

3353f337

feat(probability/probability_mass_function): construct a `pmf` from a probability measure (#18270)

dtumad committed 3 years ago

3f5c9d30

chore(measure theory/group/measure): Generalize typeclasses (#18496)

YaelDillies committed 3 years ago

950605e4

feat(number_theory/number_field/embeddings): some additional lemmas (#18473)

xroblot committed 3 years ago

271bf175

feat(measure_theory/integral): integration lemmas from #18392 (#18466)

loefflerd committed 3 years ago

733fa004

feat(analysis/convex/body): endow with Hausdorff metric (#16338)

datokrat committed 3 years ago

858a10cf

chore(data/set/basic): Golf #18356 (#18491)

YaelDillies committed 3 years ago

75608aff

feat(*/with_top): add lemmas about `with_top`/`with_bot` (#18487)

urkud committed 3 years ago

afdb4fa3

feat(geometry/manifold/vector_bundle): `smooth_fiberwise_linear` groupoid (#17302)

hrmacbeth committed 3 years ago

5be98b95

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring (#14249)

mariainesdff committed 3 years ago

a8e7ac80

chore(data/real/nnreal): drop some lemmas (#18492)

urkud committed 3 years ago

b2ff9a3d

feat(algebra/quaternion): add `quaternion.im` for the skew-adjoint part (#18456)

eric-wieser committed 3 years ago

d90149e9

refactor(data/real/ereal): add a two-argument induction principle (#18481)

eric-wieser committed 3 years ago

634284e7

feat(geometry/manifold/cont_mdiff): local structomorphisms of `cont_diff_groupoid` (#17291)

hrmacbeth committed 3 years ago

8e57ff9a

chore(*): add mathlib4 synchronization comments (#18490)

github-actions[bot] committed 3 years ago

ef7acf40

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra (#15869)

j-loreaux committed 3 years ago

651f93df

feat(topology/uniform_space/cauchy): `mul_opposite X` is complete when `X` is (#18471)

eric-wieser committed 3 years ago

22131150

refactor(algebra/{dual_number,triv_sq_zero_ext}): support non-commutative rings (#18384)

eric-wieser committed 3 years ago

b8d2eaa6

feat(model_theory/order): Renames and generalizes notation about ordered structures (#17870)

awainverse committed 3 years ago

1ed3a113

chore(category_theory/comma): removed obviously tactic for data fields (#18440)

joelriou committed 3 years ago

8a318021

Newer Older