Def DiscreteContAction

Modification history

2025-04-23 10:36

Mathlib/CategoryTheory/Action/Continuous.lean

refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` (#22574) …

Modified DiscreteContAction View on Github →

2024-05-25 10:04

Mathlib/RepresentationTheory/Action/Continuous.lean

feat(CategoryTheory/Action): category of continuous actions (#13006) …

Added DiscreteContAction View on Github →