leanprover-community/mathlib

Pull Requests Commits

agusakov committed 2 years ago

6a86b829

Merge branch 'master' of https://github.com/leanprover-community/mathlib into graphs2

agusakov committed 2 years ago

999e507a

agusakov committed 2 years ago

ea25dd85

feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301)

Vierkantor committed 2 years ago

6010cf52

refactor(linear_algebra/{general,special}_linear_group): move to matrix subfolder (#18344)

eric-wieser committed 2 years ago

ae690b0c

feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340)

eric-wieser committed 2 years ago

11b92770

refactor(data/fintype/basic): move fin_choice to a new file (#18337)

eric-wieser committed 2 years ago

d7859726

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

Older