leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 2 years ago

ae845de1

YaelDillies committed 2 years ago

0d2d7904

Merge remote-tracking branch 'origin/master' into ceva-theorem

YaelDillies committed 2 years ago

2a9ad730

feat(linear_algebra/affine_space/basis): `reindex` API (#18190)

YaelDillies committed 2 years ago

2f4cdce0

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)

loefflerd committed 2 years ago

980755c3

feat(number_theory/number_field/embeddings): add infinite_places.eq_iff (#17285)

xroblot committed 2 years ago

78ac1db3

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

leanprover-community-bot committed 2 years ago

e46da4e3

feat(topology/metric_space/isometric_smul): new file (#18130)

urkud committed 2 years ago

832a8ba8

feat(measure_theory/integral/peak_function): convergence of integral against a sequence of peak functions (#18327)

sgouezel committed 2 years ago

59694bd0

chore(algebra/char_p/basic): add char_p instances for `ulift` and `mul_opposite` (#18336)

eric-wieser committed 2 years ago

05a78c94

chore(measure_theory/integrals): API improvements for interval_integrable (#18335)

loefflerd committed 2 years ago

aa1d645a

chore(order/filter/basic): protect 3 lemmas (#18331)

urkud committed 2 years ago

24e75f1e

chore(order/upper_lower): split file (#18330)

urkud committed 2 years ago

2769416a

feat(data/quot): make `trunc` a `quotient` (#18320)

astrainfinita committed 2 years ago

6ed6abbd

feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)

MichaelStollBayreuth committed 2 years ago

afdb4342

feat(ring_theory): definition and properties of relative ideal norm (#18299)

Vierkantor committed 2 years ago

8233a1cb

chore(order/filter, topology/algebra): golf (#18097)

urkud committed 2 years ago

78f647f8

feat(algebra/periodic): generalize some lemmas (#18334)

urkud committed 2 years ago

b64b1f88

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

leanprover-community-bot committed 2 years ago

13a5329a

feat(data/{bool,set}): add 3 lemmas (#18332)

urkud committed 2 years ago

ed60ee25

refactor(topology/{order,*}): review API (#18312)

urkud committed 2 years ago

bcfa7268

chore(number_theory/cyclotomic/gal): tidy docs (#18326)

ericrbg committed 2 years ago

861a2692

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

leanprover-community-bot committed 2 years ago

68d1483e

chore(ring_theory/fractional_ideal): remove instance name (#18305)

Multramate committed 2 years ago

48cb182b

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

leanprover-community-bot committed 2 years ago

fac36901

chore(*): rename locale `topological_space` to `topology` (#18293)

urkud committed 2 years ago

f2ce6086

fix(data/set_like): unbundled subclasses of `out_param` classes should not repeat the parents' `out_param` (#18291)

Vierkantor committed 2 years ago

feb99064

feat(ring_theory): lemmas on algebra norm (#18298)

Vierkantor committed 2 years ago

5fe29816

chore(topology/metric_space/anti_lipschitz): fix typo (#18263)

JovanGerb committed 2 years ago

97f079b7

feat(ring_theory/ideal/local_ring): API for local rings. (#17185)

erdOne committed 2 years ago

b86c528d

Older