Commits leanprover-community/mathlib

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

github-actions[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)

github-actions[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)

github-actions[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)

github-actions[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)

github-actions[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)

github-actions[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)

github-actions[bot] committed 2 years ago

660b3a2d