mathlib3

07980376 - refactor(algebra/group/inj_surj): add npow and zpow to all definitions (#12126)

refactor(algebra/group/inj_surj): add npow and zpow to all definitions (#12126) Currently, we have a small handful of helpers to construct algebraic structures via pushforwards and pullbacks that preserve `has_pow` and `has_scalar` instances (added in #10152 and #10832): * `function.{inj,surj}ective.add_monoid_smul` * `function.{inj,surj}ective.monoid_pow` * `function.{inj,surj}ective.sub_neg_monoid_smul` * `function.{inj,surj}ective.div_inv_monoid_smul` * `function.{inj,surj}ective.add_group_smul` * `function.{inj,surj}ective.group_pow` Predating these, we have a very large collection of helpers that construct new `has_pow` and `has_scalar` instances, for all the above and also for every other one-argument algebraic structure (`comm_monoid`, `ring`, `linear_ordered_field`, ...). This puts the user in an awkward position; either: 1. They are unaware of the complexity here, and use `add_monoid_smul` and `add_comm_monoid` within the same file, which create two nonequal scalar instances. 2. They use only the large collection, and don't get definitional control of `has_scalar` and `has_pow`, which can cause typeclass diamonds with generic `has_scalar` instances. 3. They use only the small handful of helpers (which requires remembering which ones are safe to use), and have to remember to manually construct `add_comm_monoid` as `{..add_comm_semigroup, ..add_monoid}`. If they screw up and construct it as `{..add_comm_semigroup, ..add_zero_class}`, then they're in the same position as (1) without knowing it. This change converts every helper in the large collection to _also_ preserve scalar and power instances; as a result, these pullback and pushforward helpers once again no longer construct any new data. As a result, all these helpers now take `nsmul`, `zsmul`, `npow`, and `zpow` arguments as necessary, to indicate that these operations are preserved by the function in question. As a result of this change, all existing callers are now expected to have a `has_pow` or `has_scalar` implementation available ahead of time. In many cases the `has_scalar` instances already exist as a more general case, and maybe just need reordering within the file. Sometimes the general case of `has_scalar` is stated in a way that isn't general enough to describe `int` and `nat`. In these cases and the `has_pow` cases, we define new instance manually. Grepping reveals a rough summary of the new instances: ```lean instance : has_pow (A 0) ℕ instance has_nsmul : has_scalar ℕ (C ⟶ D) instance has_zsmul : has_scalar ℤ (C ⟶ D) instance has_nsmul : has_scalar ℕ (M →ₗ⁅R,L⁆ N) instance has_zsmul : has_scalar ℤ (M →ₗ⁅R,L⁆ N) instance has_nsmul : has_scalar ℕ {x : α // 0 ≤ x} instance has_pow : α // 0 ≤ x} ℕ instance : has_scalar R (ι →ᵇᵃ[I₀] M) instance has_nat_scalar : has_scalar ℕ (normed_group_hom V₁ V₂) instance has_int_scalar : has_scalar ℤ (normed_group_hom V₁ V₂) instance : has_pow ℕ+ ℕ instance subfield.has_zpow : has_pow s ℤ instance has_nat_scalar : has_scalar ℕ (left_invariant_derivation I G) instance has_int_scalar : has_scalar ℤ (left_invariant_derivation I G) instance add_subgroup.has_nsmul : has_scalar ℕ H instance subgroup.has_npow : has_pow H ℕ instance add_subgroup.has_zsmul : has_scalar ℤ H instance subgroup.has_zpow : has_pow H ℤ instance add_submonoid.has_nsmul : has_scalar ℕ S instance submonoid.has_pow : has_pow S ℕ instance : has_pow (special_linear_group n R) ℕ instance : has_pow (α →ₘ[μ] γ) ℕ instance has_int_pow : has_pow (α →ₘ[μ] γ) ℤ instance : div_inv_monoid (α →ₘ[μ] γ) instance has_nat_pow : has_pow (α →ₛ β) ℕ instance has_int_pow : has_pow (α →ₛ β) ℤ instance has_nat_pow : has_pow (germ l G) ℕ instance has_int_pow : has_pow (germ l G) ℤ instance : has_scalar ℕ (fractional_ideal S P) instance has_nat_scalar : has_scalar ℕ (𝕎 R) instance has_int_scalar : has_scalar ℤ (𝕎 R) instance has_nat_pow : has_pow (𝕎 R) ℕ instance has_nat_scalar : has_scalar ℕ (truncated_witt_vector p n R) instance has_int_scalar : has_scalar ℤ (truncated_witt_vector p n R) instance has_nat_pow : has_pow (truncated_witt_vector p n R) ℕ instance has_nat_scalar : has_scalar ℕ (α →ᵇ β) instance has_int_scalar : has_scalar ℤ (α →ᵇ β) instance has_nat_pow : has_pow (α →ᵇ R) ℕ ```