Def Fin.consEquivL

Modification history

2026-09-25 14:20

Mathlib/Topology/Algebra/Module/Equiv/Basic.lean

chore(Algebra/Module/Equiv): split Equiv into Basic, Pi, Prod and Submodule (#42818) …

Modified Fin.consEquivL View on Github →

2025-01-29 23:20

Mathlib/Topology/Algebra/Module/Equiv.lean

feat: `HasFDerivAt` for `Fin.cons` (#20407) …

Added Fin.consEquivL View on Github →