Skip to content

Commit

Permalink
make pre-commit
Browse files Browse the repository at this point in the history
  • Loading branch information
lowasser committed Feb 10, 2025
1 parent 38d7af2 commit 667bea2
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions src/group-theory/minkowski-multiplication-semigroups.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,12 @@ open import logic.functoriality-existential-quantification
## Idea

Given two [subsets](group-theory.subsets-semigroups.md) `A` and `B` of a
[semigroup](group-theory.semigroups.md) `S`, the {{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}} of `A`
and `B` is the [set](foundation-core.sets.md) of elements that can be formed by multiplying an element of
`A` and an element of `B`. This binary operation defines a semigroup structure on the [powerset](foundation.powersets.md) of `S`.
[semigroup](group-theory.semigroups.md) `S`, the
{{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}}
of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be
formed by multiplying an element of `A` and an element of `B`. This binary
operation defines a semigroup structure on the
[powerset](foundation.powersets.md) of `S`.

## Definition

Expand Down

0 comments on commit 667bea2

Please sign in to comment.