leanprover-community/mathlib3

Pull Requests Commits

Partial reverse to bases :/

ADedecker committed 3 years ago

7c4aeb75

ADedecker committed 3 years ago

ea16f9cf

ADedecker committed 3 years ago

2ba359ff

Merge branch 'AD_proj_basis' into AD_trace_class_3

ADedecker committed 3 years ago

37233d1b

Use `partial_span`

ADedecker committed 3 years ago

b926a532

Merge branch 'AD_hilbert_basis_partial_spans' into AD_proj_basis

ADedecker committed 3 years ago

5456e36a

Define `hilbert_basis.partial_span`

ADedecker committed 3 years ago

3863707a

Avoid bases, deep cleanup

ADedecker committed 3 years ago

97cd3bfb

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

Use general version

ADedecker committed 3 years ago

00eccd45

ADedecker committed 3 years ago

073e2a80

Merge branch 'AD_orthogonal_projection_facts' into AD_proj_basis

ADedecker committed 3 years ago

cd1d659c

Merge branch 'AD_orthogonal_projection_facts' into AD_trace_class_3

ADedecker committed 3 years ago

c14b36a3

ADedecker committed 3 years ago

59ab4dea

Various facts about `orthogonal_projection`

ADedecker committed 3 years ago

7c690c06

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

hrmacbeth committed 3 years ago

5bd49e4c

ADedecker committed 3 years ago

91ec0986

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

ADedecker committed 3 years ago

6d3977ef

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

ADedecker committed 3 years ago

e12d3a60

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

Older