leanprover-community/mathlib

Pull Requests Commits

apnelson1 committed 3 years ago

ddfb73ca

chore(data/seq/seq): clean up spacing (#15825)

vihdzp committed 3 years ago

dd6f53d8

feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. (#15036)

linesthatinterlace committed 3 years ago

1563242e

feat(data/finsupp/basic): `alist.lookup` as a finitely supported function (#15443)

vihdzp committed 3 years ago

637b58e8

refactor(linear_algebra): morphism refactor for `linear_equiv`, `continuous_linear_equiv`, `linear_isometry` and `linear_isometry_equiv` (#15078)

dupuisf committed 3 years ago

798b4ae1

feat(data/seq/seq): improve `cons` and `tail` def-eqs (#15829)

vihdzp committed 3 years ago

078cd612

feat(data/list/basic): `l.nth l.length = none` (#15828)

vihdzp committed 3 years ago

0e87ef97

chore(data/stream/defs): remove match from `stream.cons` (#15789)

pechersky committed 3 years ago

54c4c222

feat(set_theory/ordinal/arithmetic): generalize `mod_opow_log_lt_self` (#15448)

vihdzp committed 3 years ago

53ab3a54

refactor(set_theory/game/nim): remove `nim` namespace (#15366)

vihdzp committed 3 years ago

997fa572

doc(data/polynomial/basic): fix docstring (#15814)

astrainfinita committed 3 years ago

adc4ebc7

chore(probability/martingale): add some parity lemmas for martingales and supermartingales (#15811)

kex-y committed 3 years ago

777082da

feat(algebra/big_operators/multiset): add `prod_map_erase` for `list` and `multiset` (#15808)

astrainfinita committed 3 years ago

bedd9506

feat(geometry/manifold/mfderiv): differentiability is a `local_invariant_prop`, and consequences (#15666)

hrmacbeth committed 3 years ago

58004685

feat(algebraic_geometry/EllipticCurve): add 2-torsion polynomials and changes of variables (#15230)

Multramate committed 3 years ago

c06c6806

feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean (#15684)

MichaelStollBayreuth committed 3 years ago

2a2d33c8

feat(ring_theory/dedekind_domain): promote fractional ideals to `semifield` (#15794)

Vierkantor committed 3 years ago

aafeb5f3

chore(*): golf using new `positivity` tactic (#15701)

hrmacbeth committed 3 years ago

5bd49e4c

feat(algebra/algebra/bilinear): make `algebra.lmul` to apply to non-unital (non-assoc) algebras (#15310)

j-loreaux committed 3 years ago

9264b15e

lemmas about coeff for `compute_degree` (#15694)

adomani committed 3 years ago

10a5ded3

fix(algebra/monoid_algebra/basic): add `int_cast` to `monoid_algebra` instances (#15779)

ericrbg committed 3 years ago

59874523

fix(tactic/rcases): support `rcases x with y` renames (#15773)

digama0 committed 3 years ago

073a3e97

refactor(category_theory): custom structure for full_subcategory (#14767)

TwoFX committed 3 years ago

bb103f35

feat(order/rel_iso): relation embeddings for `sum.lex` and `prod.lex` (#15355)

vihdzp committed 3 years ago

7200c507

feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722)

jsm28 committed 3 years ago

674505ed

feat(algebra/order/floor): `fract_one` (#15785)

jsm28 committed 3 years ago

7dcf5c3d

chore(data/zmod): make `zmod.int_cast_zmod_cast` `@[norm_cast]` (#15753)

Vierkantor committed 3 years ago

2f1b3131

feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)

tb65536 committed 3 years ago

1b09efe3

fix(data/polynomial/basic): remove `monomial_fun` to remove diamonds (#15778)

ericrbg committed 3 years ago

7ad184e3

feat(order/succ_pred/basic): `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related (#15567)

vihdzp committed 3 years ago

9bb1256d

Older