leanprover-community/mathlib

Pull Requests Commits
partial fix
eric-wieser committed 3 years ago
b32ddda9
propagate error messages
eric-wieser committed 3 years ago
2ea0fa0a
get ext_simplify_core partially working
eric-wieser committed 3 years ago
56046c79
add Eric's example to the tests
adomani committed 3 years ago
9bf2f7e2
add refl after simp
adomani committed 3 years ago
2e2763a9
golf
adomani committed 3 years ago
7173cbf0
questions
adomani committed 3 years ago
4d90fe8a
let test
adomani committed 3 years ago
c88eeba6
typo
adomani committed 3 years ago
87fe91f8
lint
adomani committed 3 years ago
94f45dc1
add generic operation
adomani committed 3 years ago
e7a83692
update doc-module
adomani committed 3 years ago
470eaa94
Merge branch 'aa_sort' of ssh://github.com/leanprover-community/mathlib into aa_sort
adomani committed 3 years ago
052b6b8d
use replace_goal to avoid creating metavariable issues
eric-wieser committed 3 years ago
c10fa224
replace is_given_op with as_given_op
eric-wieser committed 3 years ago
73e6dc2a
add a test of metavariables
eric-wieser committed 3 years ago
883268d6
Eliminate the `lu` argument to `reorder_oper`.
eric-wieser committed 3 years ago
e3fb88c8
Update src/tactic/move_add.lean
adomani committed 3 years ago
Verified 1a47afc9
removed two spaces
adomani committed 3 years ago
93f31fad
rename
adomani committed 3 years ago
9e9794c9
fix error messages in tests
adomani committed 3 years ago
3f3ee649
formatting
adomani committed 3 years ago
29017ee4
Apply Eric's suggestions
adomani committed 3 years ago
Verified 009c686d
typo
adomani committed 3 years ago
902d6314
use alternative
adomani committed 3 years ago
f1db190d
Merge branch 'aa_sort' of ssh://github.com/leanprover-community/mathlib into aa_sort
adomani committed 3 years ago
32b82f94
Merge branch 'master' into aa_sort
adomani committed 3 years ago
ea89af8b
feat(probability_theory/independence): if a family of pi-systems is independent, then so are the generated measurable spaces (#9387)
RemyDegenne committed 3 years ago
3594b635
feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)
kex-y committed 3 years ago
728e074e
minor changes
adomani committed 3 years ago
c03b94fb
Terms Of Use Privacy Policy Refund Policy Impressum