Theorem Mathlib.Meta.Multiset.insert_eq_cons
Modification history
2024-02-04 23:05
Mathlib/Tactic/NormNum/BigOperators.lean
chore(LinearAlgebra,BigOperators): drop some decidability assumptions (#10237) …
Modified Mathlib.Meta.Multiset.insert_eq_consView on Github →