Skip to content

Commit c3e588b

Browse files
committed
chore: fix implicit-reducible diamond in Schwartz space (leanprover-community#38263)
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
1 parent 13a3aa6 commit c3e588b

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/Analysis/Distribution/SchwartzSpace

Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -530,7 +530,7 @@ instance instIsTopologicalAddGroup : IsTopologicalAddGroup 𝓢(E, F) :=
530530
(schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isTopologicalAddGroup
531531

532532
instance instUniformSpace : UniformSpace 𝓢(E, F) :=
533-
(schwartzSeminormFamily ℝ E F).addGroupFilterBasis.uniformSpace
533+
fast_instance% (schwartzSeminormFamily ℝ E F).addGroupFilterBasis.uniformSpace
534534

535535
instance instIsUniformAddGroup : IsUniformAddGroup 𝓢(E, F) :=
536536
(schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isUniformAddGroup

0 commit comments

Comments
 (0)