leanprover-community/mathlib3

Pull Requests Commits

themathqueen committed 2 years ago

c81aeeeb

themathqueen committed 2 years ago

f643232b

remove continuous_linear_map.is_positive

themathqueen committed 2 years ago

a99bdf43

themathqueen committed 2 years ago

d7ad6ab0

themathqueen committed 2 years ago

384a18e8

eric-wieser committed 2 years ago

Verified 258fe88e

themathqueen committed 2 years ago

27965f4a

themathqueen committed 2 years ago

8c90ed60

remove nonneg def

themathqueen committed 2 years ago

0500a32b

move results to new pr

themathqueen committed 2 years ago

ee544c3f

change name and remove lemma

themathqueen committed 2 years ago

e8b14bde

themathqueen committed 2 years ago

bce4f554

delete pairwise_orthogonal

eric-wieser committed 2 years ago

85b8249e

Merge branch 'master' into inner_product_space_positive

eric-wieser committed 2 years ago

Verified aca9fef4

feat(analysis/inner_product_space/basic): orthogonal submodules (#18705)

eric-wieser committed 2 years ago

1a4df69c

feat(analysis/calculus/iterated_deriv): equality of norms of iterated derivative (#18728)

mcdoll committed 2 years ago

d524d0a5

chore(linear_algebra/dimension): rename `rank` to `linear_map.rank` (#18734)

eric-wieser committed 2 years ago

be2ac64b

chore(linear_algebra/free_module/finite/rank): move lemmas from `module.free` to `finite_dimensional` (#18733)

eric-wieser committed 2 years ago

4cf7ca0e

chore(linear_algebra/finite_dimensional): generalize from Type to Sort (#18723)

eric-wieser committed 2 years ago

0ce07501

chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725)

eric-wieser committed 2 years ago

7aac545b

feat(measure_theory/function): Functions locally integrable on a set (#18673)

loefflerd committed 2 years ago

08a4542b

feat(algebra/group_power/lemmas): Induction principle for powers (#18668)

YaelDillies committed 2 years ago

e655e4ea

feat(linear_algebra/dimension): free generalizations (#18722)

eric-wieser committed 2 years ago

3cacc945

feat(ring_theory/zmod): Criterion for `zmod` to be a reduced ring (#16998)

alexjbest committed 2 years ago

00d163e3

refactor(linear_algebra): make `module.free` available inside `linear_algebra/dimension` (#18717)

eric-wieser committed 2 years ago

59628387

refactor(set_theory/cardinal/basic): redefine `cardinal.is_limit` in terms of `is_succ_limit` (#18523)

vihdzp committed 2 years ago

7c2ce0c2

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

leanprover-community-bot committed 2 years ago

94eaaaa6

feat(data/{int,nat}/modeq): `a/c ≡ b/c mod m/c → a ≡ b mod m` (#18666)

YaelDillies committed 2 years ago

47a1a733

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

leanprover-community-bot committed 2 years ago

31ca6f9c

feat(data/matrix/reflection): lemmas for arbitrary concrete matrices, proved via reflection (#18711)

eric-wieser committed 2 years ago

d95bef0d

Older