From 07157f4f43d6199ebe1da51c70d1e6d9cc06b8a0 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 24 Sep 2024 14:41:25 -0500 Subject: [PATCH] =?UTF-8?q?chore:=20fix=20type=20class=20assumptions=20for?= =?UTF-8?q?=20`NonUnitalStarAlgHom.map=5Fcfc=E2=82=99`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean index e5c7cea5ca34e..2895a56f474d3 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean @@ -428,9 +428,9 @@ open scoped ContinuousMapZero variable {F R S A B : Type*} {p : A → Prop} {q : B → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] - [Ring A] [StarRing A] [TopologicalSpace A] [Module R A] + [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] - [Ring B] [StarRing B] [TopologicalSpace B] [Module R B] + [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B] [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q]