leanprover-community/mathlib

Pull Requests Commits

golf, remove a questionable set lemma

eric-wieser committed 2 years ago

591b14e4

correct lemma name

eric-wieser committed 2 years ago

10b09f20

missing backtick

eric-wieser committed 2 years ago

f591c22e

eric-wieser committed 2 years ago

427c883a

add the general form of the lemmas

eric-wieser committed 2 years ago

7307edad

Update src/linear_algebra/general_linear_group.lean

themathqueen committed 2 years ago

Verified cb42b2a1

themathqueen committed 2 years ago

19b5ba93

changes after review

themathqueen committed 2 years ago

a2404387

themathqueen committed 2 years ago

62867498

themathqueen committed 2 years ago

accaa222

themathqueen committed 2 years ago

39168b45

changes after review

themathqueen committed 2 years ago

8ea48f4c

themathqueen committed 2 years ago

459d90b1

themathqueen committed 2 years ago

4172305b

refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (#18345)

eric-wieser committed 2 years ago

2705404e

feat(counterexamples/quadratic_form): symmetric bilinear forms in char 2 do not always inject into quadratic forms (#18146)

eric-wieser committed 2 years ago

8a035e9a

feat(analysis/special_functions/pow): strengthen cpow integrability lemmas (#18354)

loefflerd committed 2 years ago

da1d134a

feat(ring_theory/localization): remove extraneous `algebra_map_submonoid S M ≤ S⁰` conditions (#18358)

alreadydone committed 2 years ago

2e59a6de

feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187)

MantasBaksys committed 2 years ago

aebd3428

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

leanprover-community-bot committed 2 years ago

f16e7a22

chore(scripts): update nolints.txt (#18357)

leanprover-community-bot committed 2 years ago

4ef778c2

feat(analysis/special_functions/gaussian): Fourier transform of Gaussian (#18338)

loefflerd committed 2 years ago

d90e4e18

feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095)

sgouezel committed 2 years ago

b3607518

fix(algebra/lie/*): use correct terminology for `centralizer` and `normalizer` in Lie theory (#18348)

ocfnash committed 2 years ago

938fead7

feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301)

Vierkantor committed 2 years ago

6010cf52

refactor(linear_algebra/{general,special}_linear_group): move to matrix subfolder (#18344)

eric-wieser committed 2 years ago

ae690b0c

feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340)

eric-wieser committed 2 years ago

11b92770

refactor(data/fintype/basic): move fin_choice to a new file (#18337)

eric-wieser committed 2 years ago

d7859726

feat(linear_algebra/affine_space/basis): `reindex` API (#18190)

YaelDillies committed 2 years ago

2f4cdce0

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)

loefflerd committed 2 years ago

980755c3

Older