Commit 2024-04-17 07:30 66c16514

View on Github →

chore(GroupTheory): remove autoImplicit (#12134)

Estimated changes

Modified Mathlib/GroupTheory/ClassEquation.lean

Modified Mathlib/GroupTheory/CommutingProbability.lean

modified theorem commProb_function

modified theorem commProb_pi

Modified Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean

Modified Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Prod.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

modified theorem ConjClasses.card_carrier