option): Scalar action on an option (#15239)

Commit

3 years ago

feat(group_theory/group_action/option): Scalar action on an option (#15239) `has_scalar α β → has_scalar α (option β)` and similar.

Author

YaelDillies

Parents