Commit 2024-04-05 21:50 75a72d07

View on Github →

refactor: Use nsmul in zsmul_rec (#862) It's annoying that zsmulRec uses nsmulRec to define zsmul even when the user already set nsmul explicitly. This PR changes zsmulRec to take nsmul as an argument.

Estimated changes

Modified Mathlib/Algebra/Group/Aut.lean

Modified Mathlib/Algebra/Group/Defs.lean

modified def zpowRec

modified def zsmulRec

Modified Mathlib/Algebra/Ring/Aut.lean

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Set/Pointwise/Basic.lean

Modified Mathlib/NumberTheory/Dioph.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

modified theorem BoundedContinuousFunction.coe_zsmulRec

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

deleted theorem ZeroAtInftyContinuousMap.coe_nsmulRec

deleted theorem ZeroAtInftyContinuousMap.coe_zsmulRec