Commits leanprover-community/mathlib3

merge

Scott Morrison committed 2 years ago

dfab3c97

feat(measure_theory/constructions/polish): quotient group is a Borel space (#19186)

urkud committed 2 years ago

9f55d0d4

feat(data/mv_polynomial/basic): add more general smul compatibility instances (#19187)

eric-wieser committed 2 years ago

c8734e89

refactor(field_theory/polynomial_galois_group): remove `open_locale classical` (#19184)

eric-wieser committed 2 years ago

8bdf5e9b

feat(geometry/manifold/vector_bundle/smooth_section): define smooth sections (#19064)

fpvandoorn committed 2 years ago

f9ec1871

chore(*): fix `@[to_additive, simp]` to the correct order (#19169)

ericrbg committed 2 years ago

1ac8d430

chore(linear_algebra/eigenspace/minpoly): remove a silly use of `tauto` (#19183)

eric-wieser committed 2 years ago

c3216069

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

leanprover-community-bot committed 2 years ago

d07a9c87

refactor(data/polynomial/ring_division): remove `open_locale classical` (#19182)

eric-wieser committed 2 years ago

8efcf802

chore(field_theory/abel_ruffini): Rename variables (#19180)

tb65536 committed 2 years ago

fbbd626e

feat(algebraic_geometry/elliptic_curve/point): the group law on the nonsingular rational points of a Weierstrass curve (#18000)

Multramate committed 2 years ago

e2e7f2ac

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

leanprover-community-bot committed 2 years ago

44e2ae8c

refactor(representation_theory/Rep): define `ihom` concretely (#19170)

Amelia Livingston committed 2 years ago

cec81510

refactor(field_theory/splitting_field/is_splitting_field): use `root_set` (#19179)

eric-wieser committed 2 years ago

9fb89647

chore(measure_theory/function/conditional_expectation): split `measure_theory.function.conditional_expectation.basic` (#19177)

RemyDegenne committed 2 years ago

d8bbb04e

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

leanprover-community-bot committed 2 years ago

087c325a

refactor(data/nat/nth): redefine, review API (#18760)

urkud committed 2 years ago

7fdd4f37

feat(measure_theory/integral/set_integral): First moment method (#18731)

YaelDillies committed 2 years ago

ccdbfb6e

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

leanprover-community-bot committed 2 years ago

660b3a2d

chore(number_theory/legendre_symbol/gauss_eisenstein_lemmas): move zmod.wilsons_lemma (#19172)

Ruben-VandeVelde committed 2 years ago

c471da71

feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)

Multramate committed 2 years ago

90b0d53e

feat(data/polynomial/div): add X_sub_C_dvd_sub_C_eval (#19120)

Multramate committed 2 years ago

e1e7190e

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

leanprover-community-bot committed 2 years ago

fd4551cf

feat(algebra/module/zlattice): prove some results about Z-lattices (#18266)

xroblot committed 2 years ago

a3e83f0f

feat(linear_algebra/matrix/nonsingular_inverse): 2×2 block triangular matrices are invertible iff their diagonal is (#18849)

eric-wieser committed 2 years ago

96aa788f

feat(probability/martingale): optional sampling theorem (#14065)

RemyDegenne committed 2 years ago

ba074af8

chore(*/centralizer): add forgotten `to_additive`s (#19168)

ericrbg committed 2 years ago

cc67cd75

chore(modular_forms/basic): fix typo in docs (#19166)

ericrbg committed 2 years ago

59150e4a

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

leanprover-community-bot committed 2 years ago

6b31d1ee

feat(analysis/convex/cone/proper): define proper cone (#18913)

apurvnakade committed 2 years ago

74f1d619