Commits leanprover-community/mathlib3

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)

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

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

chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen (#17892)

eric-wieser committed 2 years ago

e5820f6c

chore(linear_algebra/dimension): remove a nontriviality assumption (#18715)

eric-wieser committed 2 years ago

500ccb10

chore(measure_theory/measure/doubling): rename `is_doubling_measure` to `is_unif_loc_doubling_measure` (#18709)

ocfnash committed 2 years ago

5f6e827d

feat(set_theory/cardinal/basic): clean up instances (#18714)

vihdzp committed 2 years ago

ea050b44

chore(group_theory/subgroup/basic): Protect `subgroup.subtype` (#18712)

YaelDillies committed 2 years ago

6b600207

feat(measure_theory/measurable_space): Cast of natural is measurable (#18676)

YaelDillies committed 2 years ago

88fcb83f

feat(combinatorics/additive/e_transform): e-transforms (#18683)

YaelDillies committed 2 years ago

207c9259

fix(data/nat/squarefree): `norm_num` only supports `squarefree` on naturals (#18708)

Vierkantor committed 2 years ago

3c1368ca

chore(algebra/order/lattice_group): Golf (#18046)

mans0954 committed 2 years ago

474656fd

feat(data/{set,finset}/pointwise): `a • t ⊆ s • t` (#18697)

YaelDillies committed 2 years ago

5e526d18

refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` (#15071)

vihdzp committed 2 years ago

210657c4

feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems (#2819)

alexjbest committed 2 years ago

02e095b2

feat(data/pnat/basic): pnat is a well-order (#18700)

vihdzp committed 2 years ago

172bf281

chore(analysis/locally_convex/strong_topology): generalize to semilinear maps (#18679)

mcdoll committed 2 years ago

47b12e7f