Theorem ContinuousLinearMap.coe_proj

Modification history

2025-04-07 04:49

Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

chore: tidy various files (#23665)

Modified ContinuousLinearMap.coe_proj View on Github →

2025-03-23 19:31

Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

feat(NumberField/CanonicalEmbedding/NormLeOne): Prove a change of variable formula for `expMapBasis` (#22756) …

Added ContinuousLinearMap.coe_proj View on Github →