Commits leanprover-community/mathlib3

instance

vihdzp committed 2 years ago

4fdb452f

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

feat(data/list/to_finsupp): computable finsupp from list (#15161)

pechersky committed 2 years ago

06a655b5

chore(linear_algebra/matrix/adjugate): add missing `matrix.of` wrapper (#18736)

eric-wieser committed 2 years ago

55102fc1

chore(category_theory/monad/basic): remove some simp lemmas (#18727)

kim-em committed 2 years ago

9c6816ca

refactor(linear_algebra/dimension): use `rank` in lemma names instead of `dim` (#18741)

eric-wieser committed 2 years ago

039a089d

feat(field_theory/is_alg_closed/algebraic_closure): add instances normal and is_galois for algebraic closure (#18730)

xroblot committed 2 years ago

0ac3057e

feat(analysis/schwartz_space): construction of continuous linear maps (#18651)

mcdoll committed 2 years ago

b2a5f0d6

feat(algebra/divisibility/basic): Dot notation aliases (#18698)

YaelDillies committed 2 years ago

e8638a0f

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

leanprover-community-bot committed 2 years ago

d64d67d0

chore(topology/algebra/group): generalise instances (#15171)

alexjbest committed 2 years ago

3b1890e7

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