Def ContinuousAlternatingMap.prod

Modification history

2024-03-01 17:50

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

fix: denote alternating map by ⋀, not Λ (#11064) …

Modified ContinuousAlternatingMap.prod View on Github →

2023-07-06 18:35

Mathlib/Topology/Algebra/Module/Alternating.lean

feat: define continuous alternating maps (#5678)

Added ContinuousAlternatingMap.prod View on Github →