leanprover-community/mathlib3

Pull Requests Commits

Merge branches '4e554c4c/kaehler_is_base_change', '4e554c4c/localized_module_is_tensor_product' and '4e554c4c/Mon_Ab' into 4e554c4c/adjunction_theorem

4e554c4c committed 2 years ago

fbdcc358

fix derivation.lean on recent mathlib

4e554c4c committed 2 years ago

f537ab93

Merge branch 'kaehler_is_base_change'

4e554c4c committed 2 years ago

c7b83f14

fix sheaf_monoidal.lean... kinda

4e554c4c committed 2 years ago

dab6998e

fix presheaf_monoidal.lean

4e554c4c committed 2 years ago

fdb0fdf6

fix category/Group/monoidal.lean

4e554c4c committed 2 years ago

8c95f952

Merge remote-tracking branch 'origin/master' into 4e554c4c/Mon_Ab

4e554c4c committed 2 years ago

7769cfb7

chore(order/filter/filter_product): fix `const_lt`, make `const_lt_iff` `@[simp, norm_cast]` (#17442)

astrainfinita committed 2 years ago

3592f45e

refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICULAR instead of ⊥ UP TACK (#18423)

eric-wieser committed 2 years ago

70a4f219

chore(data/finset/sym): fix a typo (#18426)

xroblot committed 2 years ago

99624c1a

chore(algebra/algebra/basic): remove a duplicate lemma (#18415)

eric-wieser committed 2 years ago

71150516

feat(topology/continuous_function): lemmas on infinite sums of continuous functions (#18424)

loefflerd committed 2 years ago

ddbfecf5

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

leanprover-community-bot committed 2 years ago

ad0089ac

feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual numbers (#18200)

eric-wieser committed 2 years ago

806c0bb8

remove useless proof

4e554c4c committed 2 years ago

5e4b4603

chore(algebra/group_with_zero/units/lemmas): `div_div_cancel_left'` (#18421)

eric-wieser committed 2 years ago

dc6c365e

feat(algebraic_geometry/elliptic_curve/point): define addition of K-rational points (#17194)

Multramate committed 2 years ago

67f92b6f

feat(measure_theory/group.measure): add pi.is_haar_measure (#18390)

xroblot committed 2 years ago

4b83fd28

chore(measure_theory/decomposition/unsigned_hahn): speedup Hahn decomposition (#18419)

sgouezel committed 2 years ago

0f1becb7

chore(algebra/quaternion): missing trivial lemmas (#18413)

eric-wieser committed 2 years ago

d3e3adc9

feat(analysis/fourier): Riemann-Lebesgue lemma (part 1) (#18361)

loefflerd committed 2 years ago

735b22f8

chore(topology/algebra): make the divisor argument of `div_const` explicit (#18411)

eric-wieser committed 2 years ago

8c8c544b

refactor(topology/sets/opens): use a `structure` for `opens` and `open_nhds_of` (#18409)

urkud committed 2 years ago

d39590fc

chore(topology/constructions): pi.single is continuous (#18412)

eric-wieser committed 2 years ago

dde670c9

feat(analysis/quaternion): add `complete_space`, `module.free`, and `module.finite` instances (#18347)

eric-wieser committed 2 years ago

24f7dbdf

feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395)

sgouezel committed 2 years ago

a7589864

feat(analysis/special_functions/trigonometric/series): express `cos`/`sin` as infinite sums (#18352)

eric-wieser committed 2 years ago

ccf84e0d

chore(*): remove default.lean files that had nothing but imports (#18408)

urkud committed 2 years ago

916aaa16

chore(topology/algebra/infinite_sum): correct argument explicitness (#18403)

eric-wieser committed 2 years ago

639b66d9

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

leanprover-community-bot committed 2 years ago

b6da1a0b

Older