Skip to content

Rename homo to ∙-homo in Algebra.Morphism.Structures #1013

Rename homo to ∙-homo in Algebra.Morphism.Structures

Rename homo to ∙-homo in Algebra.Morphism.Structures #1013

Triggered via pull request January 29, 2025 12:01
Status Success
Total duration 16s
Artifacts

whitespace.yml

on: pull_request
check-whitespace
5s
check-whitespace
Fit to window
Zoom out
Zoom in