Skip to content

generalize SimpleFun codomain from realType to sigmaRingType#1988

Open
hoheinzollern wants to merge 5 commits into
math-comp:masterfrom
hoheinzollern:sfun-codomain-sigmaring
Open

generalize SimpleFun codomain from realType to sigmaRingType#1988
hoheinzollern wants to merge 5 commits into
math-comp:masterfrom
hoheinzollern:sfun-codomain-sigmaring

lmodType structure on simple functions valued in a normed module

b7882a9
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
rocq-core
succeeded Jun 6, 2026 in 1m 11s