leanprover-community/mathlib3

Pull Requests Commits

feat(linear_algebra/finite_dimensional): generalize results to `module.finite` (#18811)

eric-wieser committed 2 years ago

e95e4f92

feat(algebra/order/sub/defs): make `has_ordered_sub` a Prop (#18810)

kbuzzard committed 2 years ago

de29c328

feat(data/matrix/basic): more lemmas about submatrix (#18738)

eric-wieser committed 2 years ago

0e2aab2b

feat(analysis/calculus/cont_diff_def): no continuity is needed for has_ftaylor_series_up_to if n = ∞ (#18808)

mcdoll committed 2 years ago

2cf3ee29

feat(data/matrix/reflection): add `mul_vec` and `vec_mul` (#18805)

eric-wieser committed 2 years ago

820b2296

chore(analysis/seminorm): add new le_def/lt_def and renaming (#18801)

mcdoll committed 2 years ago

7ebf83ed

refactor(linear_algebra/matrix/rank): remove `decidable_eq` arguments (#18800)

eric-wieser committed 2 years ago

86add5ce

chore(linear_algebra/free_module/rank): golf a slow proof (#18804)

eric-wieser committed 2 years ago

465d4301

feat(data/matrix/rank): rank of multiplication (#18784)

eric-wieser committed 2 years ago

47a5f818

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

Newer Older