Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-07 22:26
6a4fb6e9
View on Github →
fix: use withMainContext in
linear_combination
(
#2072
) As
reported on Zulip
.
Estimated changes
Modified
Mathlib/Tactic/LinearCombination.lean
Modified
test/linear_combination.lean
added
def
g