leanprover-community/mathlib3

Pull Requests Commits

feat(linear_algebra/matrix/dot_product): `dot_product_self_eq_zero` (#18783)

eric-wieser committed 2 years ago

46822d96

chore(ring_theory/finiteness): generalize `finite_dimensional_range` to modules (#18787)

eric-wieser committed 2 years ago

039ef89b

chore(analysis/inner_product_space/symmetric): change lemma name (#18777)

themathqueen committed 2 years ago

23b80727

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

leanprover-community-bot committed 2 years ago

25a9423c

feat(analysis/calculus/cont_diff_def): C^(n+1) iff C^n derivative (#18767)

mcdoll committed 2 years ago

a493616c

refactor(topology.continuous_function.algebra): Loosen continuous_subsemiring hypothesis (#18790)

mans0954 committed 2 years ago

37ffa4ee

ci: fix label name for ported files (#18788)

eric-wieser committed 2 years ago

c9236f47

feat(measure_theory/function/continuous_map_dense): compactly supported functions are dense in L^p (#18710)

loefflerd committed 2 years ago

a8c97ed3

chore(algebra/group_with_zero/units/basic): Deduplicate instance (#18785)

YaelDillies committed 2 years ago

df5e9937

feat(analysis/calculus/cont_diff): smoothness from Taylor series (#18768)

mcdoll committed 2 years ago

0a0b3b41

feat(analysis/schwartz_space): 1-dimensional derivative (#18745)

mcdoll committed 2 years ago

8cab1cd8

feat(.github/workflows): add modifies ported label automatically (#18782)

alexjbest committed 2 years ago

9c444b9f

chore(set_theory/cardinal/basic): less awkward placement of theorems (#18771)

vihdzp committed 2 years ago

e05ead79

refactor(linear_algebra/matrix/finite_dimensional): deduplicate (#18770)

eric-wieser committed 2 years ago

b1c23399

chore(linear_algebra/dimension): tidy lemma names for `linear_map.rank` (#18769)

eric-wieser committed 2 years ago

45ce3929

chore(linear_algebra/alternating,topology/algebra/module/multilinear): add a fun_like instance (#18766)

eric-wieser committed 2 years ago

284fdd29

feat(analysis/inner_product_space/symmetric): Polarization for `is_R_or_C` (#18397)

themathqueen committed 2 years ago

36172d66

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

leanprover-community-bot committed 2 years ago

19cb3751

feat(linear_algebra/matrix/rank): generalize to rings (#18748)

eric-wieser committed 2 years ago

8535b76e

chore(category_theory): simps should not add hom lemmas (#18742)

kim-em committed 2 years ago

2efd2423

chore(linear_algebra/dimension): remove outdated comment (#18759)

eric-wieser committed 2 years ago

3a2039ad

chore(order/rel_iso/basic): better `namespace` management (#18758)

vihdzp committed 2 years ago

f29120f8

feat(number_theory/pell): add API for solutions (#18626)

MichaelStollBayreuth committed 2 years ago

dc65937e

chore(set_theory/cardinal/basic): missing lemmas about `<`/`≤` and `lift c`/`↑n` (#18752)

eric-wieser committed 2 years ago

9dba31df

feat(linear_algebra/finrank): generalize finrank to ring in more places (#18716)

eric-wieser committed 2 years ago

5ec62c81

chore(set_theory/cardinal/basic): missing lemmas about `lift c < ℵ₀` and `ℵ₀ < lift c` (#18746)

eric-wieser committed 2 years ago

e08a42b2

chore(linear_algebra/dimension): fix lemma names (#18747)

eric-wieser committed 2 years ago

67e606ea

feat(number_theory/number_field/canonical_embedding): add canonical embedding (#17783)

YaelDillies committed 2 years ago

60da01b4

chore(linear_algebra/dimension): deduplicate lemmas (#18743)

eric-wieser committed 2 years ago

5aa3c1de

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

leanprover-community-bot committed 2 years ago

75be6b61

Newer Older