leanprover-community/mathlib3

Pull Requests Commits

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

Multramate committed 2 years ago

e064a7bf

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

MichaelStollBayreuth committed 2 years ago

c23aca35

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

loefflerd committed 2 years ago

3353f337

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

dtumad committed 2 years ago

3f5c9d30

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

YaelDillies committed 2 years ago

950605e4

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

xroblot committed 2 years ago

271bf175

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

loefflerd committed 2 years ago

733fa004

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

datokrat committed 2 years ago

858a10cf

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

YaelDillies committed 2 years ago

75608aff

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

urkud committed 2 years ago

afdb4fa3

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

hrmacbeth committed 2 years ago

5be98b95

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

mariainesdff committed 2 years ago

a8e7ac80

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

urkud committed 2 years ago

b2ff9a3d

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

eric-wieser committed 2 years ago

d90149e9

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

eric-wieser committed 2 years ago

634284e7

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

hrmacbeth committed 2 years ago

8e57ff9a

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

github-actions[bot] committed 2 years ago

ef7acf40

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

j-loreaux committed 2 years ago

651f93df

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

eric-wieser committed 2 years ago

22131150

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

eric-wieser committed 2 years ago

b8d2eaa6

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

awainverse committed 2 years ago

1ed3a113

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

joelriou committed 2 years ago

8a318021

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

leanprover-community-bot committed 2 years ago

296726c9

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

github-actions[bot] committed 2 years ago

3dadefa3

feat(topology/continuous_function): some lemmas spun off from #18392 (#18465)

loefflerd committed 2 years ago

6efec6bb

feat(docs): allow deeper nesting within undergrad.yaml (#18407)

eric-wieser committed 2 years ago

3ade05ac

fix(group_theory/nielsen_schreier): fix typo (#18483)

ChrisHughes24 committed 2 years ago

1bda4fc5

feat(analysis/normed): `mul_opposite X` inherits the same norm as `X`. (#18470)

eric-wieser committed 2 years ago

335232c7

feat(data/set): add lemmas about `powerset` of `insert` and `singleton` (#18356)

joneugster committed 2 years ago

45501380

feat(linear_algebra/affine_space/affine_subspace): `⊥ < affine_span k s ↔ s.nonempty` (#18170)

YaelDillies committed 2 years ago

b875cbb7

Older