Zulip Chat Archive

Stream: mathlib4

Topic: Fintype.prod_of_injective argument names

Martin Dvořák (Mar 21 2024 at 17:31):

I think docs#Fintype.prod_of_injective has inconsistent argument names.

Yaël Dillies (Mar 21 2024 at 17:34):

You're welcome to open a PR

Martin Dvořák (Mar 21 2024 at 17:39):

Should I rename hf or the maps?

Martin Dvořák (Mar 21 2024 at 17:42):

Looking at other lemmas in the file, hf should be renamed.

Yaël Dillies (Mar 21 2024 at 17:44):

hf

Martin Dvořák (Mar 21 2024 at 17:49):

#11571

Last updated: May 02 2025 at 03:31 UTC