leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/AD_sum_inner_mul_inner' into AD_trace_class

ADedecker committed 3 years ago

9f5101de

Merge remote-tracking branch 'origin/AD_orthonormal_basis_span' into AD_trace_class

ADedecker committed 3 years ago

57ca222e

Merge remote-tracking branch 'origin/AD_linear_isometry_equiv_of_eq' into AD_trace_class

ADedecker committed 3 years ago

3754057a

Merge remote-tracking branch 'origin/AD_positive_operator' into AD_trace_class

ADedecker committed 3 years ago

b0ff20f9

ADedecker committed 3 years ago

eb27e9cb

Compute inner product in a given basis

ADedecker committed 3 years ago

5fd0e1d8

feat(data/{finset,set}/basic): `insert a s = s ↔ a ∈ s` (#15493)

YaelDillies committed 3 years ago

5a017443

chore(data/json): add a missing subtype parser for nullable types (#15486)

eric-wieser committed 3 years ago

9540a420

feat(topology/basic): add 2 lemmas about `locally_finite` families (#15485)

urkud committed 3 years ago

3557e4dc

feat(data/list/infix): drop_while and take_while suf/prefix (#15473)

pechersky committed 3 years ago

a26b4ee8

chore(algebra/group/ulift): add missing lemmas about pow, additivize (#15469)

eric-wieser committed 3 years ago

925d8909

fix(analysis/locally_convex): weaken assumptions for `totally_bounded.is_vonN_bounded` (#15468)

ADedecker committed 3 years ago

8d2ae95f

doc(set_theory/ordinal/cantor_normal_form): implementation notes (#15466)

vihdzp committed 3 years ago

2cdc7579

refactor(tactic/polyrith): use the autogenerated json parser (#15429)

eric-wieser committed 3 years ago

92f31fbc

feat(set_theory/cardinal/ordinal): cardinality of `α →₀ β` (#15198)

vihdzp committed 3 years ago

0b673ed4

feat(data/vector/mem): Lemmas about membership in a vector (#15154)

dtumad committed 3 years ago

f5d916a6

feat(data/nat/choose/basic): Definition of `multichoose` and basic lemmas (#15072)

stuart-presnell committed 3 years ago

4af7cb21

ADedecker committed 3 years ago

9fe498b2

ADedecker committed 3 years ago

de2f57ef

feat(ring_theory/bezout): Bezout domains are integrally closed (#15424)

erdOne committed 3 years ago

7b43177d

refactor(order/compactly_generated): Generalize `submodule.exists_finset_of_mem_supr` to compact elements of complete lattices (#15419)

tb65536 committed 3 years ago

ee72cf62

feat(ring_theory/localization/basic): section of localisation of non-zero is non-zero (#15404)

Multramate committed 3 years ago

0e30f2da

feat(algebraic_geometry/EllipticCurve): simplify definition of discriminant (#15365)

digama0 committed 3 years ago

582e6672

refactor(data/finset/lattice): sup' and inf' without option (#15195)

pechersky committed 3 years ago

bcc2c4e4

feat(tactic/congrm): add "function underscores" to `congrm` (#14532)

adomani committed 3 years ago

9c7a7cca

feat(algebra/module/localized_module): construction of module localisation (#14470)

jjaassoonn committed 3 years ago

fba86201

Use cod_restrict

ADedecker committed 3 years ago

25f54cbd

ADedecker committed 3 years ago

d9e16271

feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981)

riccardobrasca committed 3 years ago

903e8941

Apply suggestions from code review

ADedecker committed 3 years ago

Verified f7d21b21

Older