leanprover-community/mathlib3

Pull Requests Commits
feat(analysis/inner_product_space/l2_space): compute orthogonal projection on U given a hilbert basis of U (#15541)
ADedecker committed 3 years ago
1313934b
Switch from subtype to using set for the subspace of X
mlavrent committed 3 years ago
3b49f096
feat(algebra/module/basic): More general `smul_ne_zero` (#16608)
YaelDillies committed 3 years ago
3b727dc2
chore(category_theory/preadditive/biproducts): speed up biprod.of_components_eq (#16516)
Ruben-VandeVelde committed 3 years ago
8f09a402
feat(order/symm_diff): Heyting bi-implication (#16544)
YaelDillies committed 3 years ago
8cd94b84
Add doc comments and clean up
mlavrent committed 3 years ago
9a5ce07f
Finish it up
mlavrent committed 3 years ago
76889591
Clean up epi/mono in groupoid proofs
mlavrent committed 3 years ago
79ea5bd9
chore(tactic/{core + compute_degree}): tightening up compute_degree_le (#15649)
adomani committed 3 years ago
2d915e4e
feat(data/complex/basic): bundle complex.abs (#16347)
ericrbg committed 3 years ago
ba80091d
Add basic id, comp lemmas to help dealing with top
mlavrent committed 3 years ago
d4d3f734
Do some stuff
mlavrent committed 3 years ago
6b6c69de
chore(scripts): update nolints.txt (#16618)
leanprover-community-bot committed 3 years ago
5947fb69
Clean up split mono/split epi theorem proofs to simplify
mlavrent committed 3 years ago
7776bbc1
chore(linear_algebra/matrix/adjugate): remove unnecessary fin_cases with (#16605)
kim-em committed 3 years ago
44eb23a5
Restructure to work more consistently
mlavrent committed 3 years ago
62569f09
Formatting
mlavrent committed 3 years ago
db1e8360
Fix
mlavrent committed 3 years ago
28d51480
Remove unfinished stuff for now
mlavrent committed 3 years ago
b3234a44
chore(data/finset/basic): Scope variables over smaller sections (#16613)
eric-wieser committed 3 years ago
ac01c538
Clean up sorry's
mlavrent committed 3 years ago
9f706092
feat(algebra/punit_instances): linear_ordered_add_comm_monoid_with_top punit (#16609)
ericrbg committed 3 years ago
27b90386
chore(docs): run `bibtool` on `references.bib` (#16606)
eric-wieser committed 3 years ago
01894cc4
feat(topology/separation): connected sets in a t1 space are infinite (#16584)
ericrbg committed 3 years ago
8deb2a68
doc(group_theory/sylow): update docstring to include card_eq_multiplicity as a main result (#14354)
ChrisHughes24 committed 3 years ago
e1783b0f
Clean up main definitions docs
mlavrent committed 3 years ago
8af18ffd
More formatting and clarification comment
mlavrent committed 3 years ago
f54b8bb1
Add doc comments
mlavrent committed 3 years ago
d27a061c
finish proving epi_of_retraction
mlavrent committed 3 years ago
bc06b2da
feat(group_theory/group_action): define `distrib_smul` and `smul_zero_class` (#16123)
Vierkantor committed 3 years ago
8f66240c
Terms Of Use Privacy Policy Refund Policy Impressum