Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

S139 alias #793

Merged
merged 3 commits into from
Oct 11, 2024
Merged

S139 alias #793

merged 3 commits into from
Oct 11, 2024

Conversation

StevenClontz
Copy link
Member

@StevenClontz StevenClontz commented Oct 10, 2024

Addresses #792

@prabau
Copy link
Collaborator

prabau commented Oct 10, 2024

The additional alias is fine.

But I would have left lines 14-15 that you deleted. (In particular because it makes clear that we mean a wedge sum of countably many things, versus a (wedge sum of things) where the whole thing happens to be countable.) We could even add to that sentence something like See {{wikipedia:Wedge_sum}}.

@prabau
Copy link
Collaborator

prabau commented Oct 10, 2024

Added bouquet terminology. How does that look?

@StevenClontz
Copy link
Member Author

It's fine with me; I left it out as it felt redundant with the canonical name we're using, but it at least does no harm if you think it's best left in the description as well.

@prabau prabau merged commit ea9ca0d into main Oct 11, 2024
1 check passed
@prabau prabau deleted the StevenClontz-patch-2 branch October 11, 2024 01:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants