Commits leanprover-community/mathlib3

Merge remote-tracking branch 'origin/master' into hrmacbeth-riemannian2

hrmacbeth committed 2 years ago

adcc8f84

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

leanprover-community-bot committed 2 years ago

f2ad3645

refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not structure (#19147)

hrmacbeth committed 2 years ago

86c29aef

chore(data/zmod/algebra): make zmod.algebra a def (#19197)

riccardobrasca committed 2 years ago

0723536a

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

leanprover-community-bot committed 2 years ago

e160cefe

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

leanprover-community-bot committed 2 years ago

2a0ce625

feat(algebra/homology/local_cohomology): Add equivalence of local cohomology along cofinal diagrams (#19105)

jakelev committed 2 years ago

893964fc

feat(order/bounded_order): The lattice of complemented elements (#16267)

YaelDillies committed 2 years ago

22c4d2ff

feat(order/sup_indep): More lemmas (#11932)

YaelDillies committed 2 years ago

c4c2ed62

style(archive.100-theorems-list.xx_theorem_name): rename to `wiedijk_100_theorems.theorem_name` (#19195)

Komyyy committed 2 years ago

5563b1b4

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

leanprover-community-bot committed 2 years ago

cff8231f

chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files (#19193)

kim-em committed 2 years ago

5b2fe805

feat(field_theory/ratfunc): The numerator and denominator of a rational function are coprime (#18652)

YaelDillies committed 2 years ago

bf9bbbcf

chore(algebraic_geometry/Scheme): remove @[simps] from Spec (#19188)

kim-em committed 2 years ago

88474d1b

chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again (#19191)

riccardobrasca committed 2 years ago

4b05d3f4

chore(field_theory/splitting_field): refactor `splitting_field` (#19178)

riccardobrasca committed 2 years ago

e3f4be1f

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

leanprover-community-bot committed 2 years ago

8af7091a

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