Repository navigation

Sfun codomain sigmaring - #2170

Open

affeldt-aist wants to merge 38 commits into

math-comp:masterfrom

affeldt-aist:sfun-codomain-sigmaring

Open

Sfun codomain sigmaring#2170
affeldt-aist wants to merge 38 commits into
math-comp:masterfrom
affeldt-aist:sfun-codomain-sigmaring

Commits on Nov 10, 2026
- sigma-algebra for normed modules + sfun codomain sigma ring & module structure
  adjevahi
  committed
  6526d2b
- added image_indic_lmod_sub
  adjevahi
  committed
  5e79d43
- rebase
  arthurd
  committed
  de4f13a
- small fixes
  arthurd
  committed
  bf3fdfd
Commits on Nov 12, 2026
- add normedtype_measure.v
  affeldt-aist
  committed
  d5cfc55
- changelog
  affeldt-aist
  committed
  5e2fb8d
- fix changelog
  affeldt-aist
  committed
  893c162
- improvement?
  affeldt-aist
  committed
  9661ebe
- generalize SimpleFun codomain from realType to sigmaRingType
  
  authored and
  affeldt-aist
  committed
  9cb23cc
- generalize fctD and fctN codomain from pzRingType to nmodType and zmodType
  
  authored and
  affeldt-aist
  committed
  abf11fd
- 80 char limit
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  b8a1dbf
- add Borel sigma-algebra wrapper borel_type and measurable singletons
  
  authored and
  affeldt-aist
  committed
  0e8d64b
- lmodType structure on simple functions valued in a normed module
  
  authored and
  affeldt-aist
  committed
  73372b3
- added doc
  
  adjevahi
  authored and
  affeldt-aist
  committed
  fcecb86
- copy on borel_type
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  c5590e8
- drop borel_type wrap on sfun_op and submodule structure
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  92bffaf
- started work on top of pr 1988
  
  adjevahi
  authored and
  affeldt-aist
  committed
  b8bcd17
- generalize SimpleFun codomain from realType to sigmaRingType
  
  authored and
  affeldt-aist
  committed
  9fb4b86
- 80 char limit
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  62d50f6
- add Borel sigma-algebra wrapper borel_type and measurable singletons
  
  authored and
  affeldt-aist
  committed
  ad5f375
- generalize SimpleFun codomain from realType to sigmaRingType
  
  authored and
  affeldt-aist
  committed
  94d09c4
- copy on borel_type
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  75316cd
- started work on top of pr 1988
  
  adjevahi
  authored and
  affeldt-aist
  committed
  ab23af5
- merge with measurableTypeNormed
  
  adjevahi
  authored and
  affeldt-aist
  committed
  19fcef9
- started adding bochner.v
  
  adjevahi
  authored and
  affeldt-aist
  committed
  eb07cc9
- clean-up
  
  adjevahi
  authored and
  affeldt-aist
  committed
  3479607
- generalize SimpleFun codomain from realType to sigmaRingType
  
  authored and
  affeldt-aist
  committed
  217e352
- 80 char limit
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  9c8a0cf
- add Borel sigma-algebra wrapper borel_type and measurable singletons
  
  authored and
  affeldt-aist
  committed
  061da84
- lmodType structure on simple functions valued in a normed module
  
  authored and
  affeldt-aist
  committed
  40b514b
- added doc
  
  adjevahi
  authored and
  affeldt-aist
  committed
  19a98f9
- copy on borel_type
  
  hoheinzollern
  authored and
  affeldt-aist
  committed
  fa5c81f
- started work on top of pr 1988
  
  adjevahi
  authored and
  affeldt-aist
  committed
  cb4559b
Commits on Nov 13, 2026
- merge with measurableTypeNormed
  
  adjevahi
  authored and
  affeldt-aist
  committed
  b4cb7c1
- started adding bochner.v
  
  adjevahi
  authored and
  affeldt-aist
  committed
  1b46692
- clean-up
  
  adjevahi
  authored and
  affeldt-aist
  committed
  1c9f229
- junk
  
  brixfoly
  authored and
  affeldt-aist
  committed
  97513a6
- file mode
  affeldt-aist
  committed
  39d1455

Commits

Commits on Nov 10, 2026

Commits on Nov 12, 2026

Commits on Nov 13, 2026