Commit 2024-06-06 04:20 4ae9fd49

View on Github →

feat: obtain a non-unital continuous functional calculus from a unital one (#13541) Co-authored by: @ADedecker

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

added theorem Set.range_one

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.val_comp_inclusion

Modified Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean