Skip to content

Commit c81c5cb

Browse files
committed
doc: fix the docstring of IsTopologicalTorsor (leanprover-community#41780)
The docstring incorrectly refers to `+ᵥ` and `-ᵥ` instead of their multiplicative versions.
1 parent abb2282 commit c81c5cb

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Topology/Algebra/Group/Torsor.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ class IsTopologicalAddTorsor {V : Type*} [AddGroup V] [TopologicalSpace V]
2828
(P : Type*) [AddTorsor V P] [TopologicalSpace P] extends ContinuousVAdd V P where
2929
continuous_vsub : Continuous (fun x : P × P => x.1 -ᵥ x.2)
3030

31-
/-- A topological torsor over a topological group is a torsor where `+ᵥ` and `-ᵥ` are continuous. -/
31+
/-- A topological torsor over a topological group is a torsor where `` and `/ₛ` are continuous. -/
3232
@[to_additive]
3333
class IsTopologicalTorsor {V : Type*} [Group V] [TopologicalSpace V]
3434
(P : Type*) [Torsor V P] [TopologicalSpace P] extends ContinuousSMul V P where

0 commit comments

Comments
 (0)