Sitelet https://github.com/math-comp/math-comp/issues/1452
Skip to content

Document to_multiplicative in the header #1452

Open
Open
Document to_multiplicative in the header#1452
Labels
kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...

Description

@CohenCyril
CohenCyril
opened on Aug 20, 2025

math-comp/boot/nmodule.v

Line 176 in 18c374d

Definition to_multiplicative := @id Type.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions