leanprover-community/mathlib

Pull Requests Commits

Expand subtype in `out_hom` and clean-up proofs

0art0 committed 3 years ago

ff782dbb

bottine committed 3 years ago

0d1b4c38

bottine committed 3 years ago

baecb969

Update src/combinatorics/simple_graph/ends/defs.lean

bottine committed 3 years ago

Verified fb3f2f8c

bottine committed 3 years ago

812364d2

bottine committed 3 years ago

b7d462df

bottine committed 3 years ago

2529a2c0

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

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

Older