search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.57k stars 343 forks source link

Porting note: was `simp` #10745

Open pitmonticone opened 9 months ago

pitmonticone commented 9 months ago

Classifies porting notes claiming was simp.

Examples

https://github.com/leanprover-community/mathlib4/blob/21472664c54bb6e7fe4a120aefa52cf212be8d7c/Mathlib/Algebra/Lie/Engel.lean#L175-L186

https://github.com/leanprover-community/mathlib4/blob/21472664c54bb6e7fe4a120aefa52cf212be8d7c/Mathlib/Data/IsROrC/Basic.lean#L589-L592

https://github.com/leanprover-community/mathlib4/blob/21472664c54bb6e7fe4a120aefa52cf212be8d7c/Mathlib/LinearAlgebra/Isomorphisms.lean#L135-L141

https://github.com/leanprover-community/mathlib4/blob/21472664c54bb6e7fe4a120aefa52cf212be8d7c/Mathlib/SetTheory/Cardinal/Basic.lean#L1358-L1363

grunweg commented 7 months ago

Some of these are resolved in #12128.