Skip to content

why is prodnormedzmodule.v inside the reals package?! #2084

Open
#2097
Open
why is prodnormedzmodule.v inside the reals package?!#2084
#2097
Labels
question ❓There is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the library
Milestone
1.18.0

Description

@affeldt-aist
affeldt-aist
opened on Aug 17, 2026

analysis/reals/prodnormedzmodule.v

Line 8 in f694551

(* This file equips the product of two normedZmodTypes with a canonical *)

at least, this should be moved to normedmodtype_theory

fyi: @CohenCyril

Metadata

Metadata

Assignees

No one assigned

    Labels

    question ❓There is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions