leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_generated_bornology

ADedecker committed 2 years ago

76f15230

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

github-actions[bot] committed 2 years ago

9a48a083

feat(data/matrix/rank): rank of a matrix is the rank of its column space (#18778)

eric-wieser committed 2 years ago

21407283

chore(linear_algebra/matrix/dot_product): weaken typeclasses (#18798)

eric-wieser committed 2 years ago

5ac1dab1

chore(linear_algebra/finrank): backport removal of simp lemmas (#18794)

kim-em committed 2 years ago

347636a7

feat(linear_algebra/free_module/finite/rank): remove `module.free` assumption (#18792)

eric-wieser committed 2 years ago

b5b5dd5a

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

github-actions[bot] committed 2 years ago

814d76e2

chore(set_theory/cardinal/basic): reinstate `partial_order` (#18781)

vihdzp committed 2 years ago

9bb28972

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)

github-actions[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)

github-actions[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

Older