Commits leanprover-community/mathlib

refactor(algebra/algebra/{pi,prod}): extract into new files (#17853)

eric-wieser committed 3 years ago

3c72a10e

refactor(data/finset/image): split out of data/finset/basic (#17852)

eric-wieser committed 3 years ago

cabb8aee

feat(algebra/algebraic_card): prove `algebraic.cardinal_mk_lift_of_infinite` (#17742)

urkud committed 3 years ago

40494fe7

chore(algebra/ring/defs): generalize is_domain (#17831)

riccardobrasca committed 3 years ago

6b2e62b5

chore(algebra/order/group): Restore basic instances (#17810)

YaelDillies committed 3 years ago

55bbb807

chore(data/fintype/*): move `nat.infinite` to `fintype.card` (#17745)

urkud committed 3 years ago

eb1f1ac6

fix(scripts/add_port_comments): do not insert extra blank lines (#17850)

eric-wieser committed 3 years ago

5a61ec7d

feat(model_theory/*): Background for realized types (#17847)

awainverse committed 3 years ago

d565b3df

feat(data/set/pointwise/interval): generalize some lemmas (#17837)

urkud committed 3 years ago

68d09c58

feat(linear_algebra/affine_space/combination): explicit weights for points, subtractions and `line_map` (#17660)

jsm28 committed 3 years ago

48765fae

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

joelriou committed 3 years ago

4dc134b9

feat(ring_theory/multiplicity,data/polynomial): add some `iff`s (#17731)

urkud committed 3 years ago

3d32bf9c

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

leanprover-community-bot committed 3 years ago

1f93c643

refactor(data/set/basic): move image, preimage, and range to a new file (#17842)

eric-wieser committed 3 years ago

1b36dabc

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

joelriou committed 3 years ago

5f68029a

feat(data/zmod): a lemma on `zmod.val_min_abs` on negations (#17584)

javra committed 3 years ago

75bf5660

feat(topology/algebra/uniform_ring): add dense_inducing.extend_hom (#17212)

xroblot committed 3 years ago

ed5ef408

chore(data/set/bool_indicator): split to a new file (#17841)

eric-wieser committed 3 years ago

a43fe8bc

chore(data.nat.prime): reduce imports (#17840)

Ruben-VandeVelde committed 3 years ago

7ab3af8f

feat(data/bool/count): new file (#17621)

urkud committed 3 years ago

48c518de

feat(analysis/convex/between): spans and `Ici`, `Ioi` images (#17601)

jsm28 committed 3 years ago

54293c4c

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