Commits leanprover-community/mathlib

Merge branch 'eric-wieser/ring_con' of github.com:leanprover-community/mathlib into eric-wieser/ring_con

eric-wieser committed 3 years ago

4e5ef701

Merge remote-tracking branch 'origin/master' into eric-wieser/ring_con

eric-wieser committed 3 years ago

7c19ca90

feat(group_theory/congruence): add smul and vadd instances (#17834)

eric-wieser committed 3 years ago

6ce70381

feat(analysis/inner_product_space): promote implications to iffs (#17727)

eric-wieser committed 3 years ago

e99e8c89

feat(ring_theory/ideal/associated_prime): Define associated primes of a module. (#17065)

erdOne committed 3 years ago

a652f6c3

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure (#16931)

Multramate committed 3 years ago

5405d294

feat(algebraic_topology/dold_kan): starting the definition of the counit isomorphism of the Dold-Kan equivalence (#17619)

joelriou committed 3 years ago

5b828414

feat(analysis/calculus/bump_function_findim): show that any open set is the support of a smooth function (#17681)

sgouezel committed 3 years ago

2fe1f93c

feat(src/algebraic_geometry/morphisms/open_immersion): New file (#17591)

erdOne committed 3 years ago

68fa0fd2

feat(analysis/convex/strict_convex_between): betweenness and strictly convex spaces (#17528)

jsm28 committed 3 years ago

e1730698

feat(algebraic_geometry/Spec): `(f∗ 𝒪ₛ)ₚ` is just the localization `Sₚ` for affine `f : Spec S ⟶ Spec R` (#17471)

erdOne committed 3 years ago

4f785b62

feat(ring_theory/ring_hom_properties) : Redefine `stable_under_base_change` in terms of `is_pushout`. (#15805)

erdOne committed 3 years ago

b5aecf07

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

leanprover-community-bot committed 3 years ago

544afa1c

refactor(data/set/n_ary): extract from data/set/basic (#17836)

eric-wieser committed 3 years ago

655994e2

more lemmas

eric-wieser committed 3 years ago

2ab0504c

refactor(ring_theory/ideal/quotient): abstract a `ring_con` structure, to be used for `ring_quot` too

eric-wieser committed 3 years ago

3c63314a

more lemmas

eric-wieser committed 3 years ago

3fb7e4a0

feat(geometry/euclidean/circumcenter): reindexing (#17830)

jsm28 committed 3 years ago

07fee0ca

feat(geometry/euclidean/angle/oriented/affine): angles in pairs of parallel lines (#17829)

jsm28 committed 3 years ago

03c860eb

chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821)

urkud committed 3 years ago

0d17cfb6

feat(data/nat/log): review/extend API (#17809)

urkud committed 3 years ago

dc9db541

feat(analysis/convex/between): betweenness in a ring (#17755)

jsm28 committed 3 years ago

41abcdc0

feat(linear_algebra/affine_space/combination): `congr` lemmas (#17659)

jsm28 committed 3 years ago

514ff6b4

feat(linear_algebra/affine_space/finite_dimensional): collinearity and spans of two points (#17635)

jsm28 committed 3 years ago

ab845455

feat(geometry/euclidean/angle/unoriented/affine): collinearity lemma (#17634)

jsm28 committed 3 years ago

2af8cec7

feat(geometry/euclidean/circumcenter): equal circumspheres among cospherical points (#17572)

jsm28 committed 3 years ago

a5abf903

feat(analysis/convex/between): more transitivity variants (#17527)

jsm28 committed 3 years ago

164690af

refactor(ring_theory/ideal/quotient): abstract a `ring_con` structure, to be used for `ring_quot` too

eric-wieser committed 3 years ago

b2ee143a

feat(algebra/cubic_discriminant): add nat degree and monic lemmas (#17780)

Multramate committed 3 years ago

6f11155d

feat(geometry/euclidean/angle/oriented): base angles of isosceles triangles are acute (#17823)

jsm28 committed 3 years ago

10ac9529