Commit 2025-06-07 01:53 b864ec45

View on Github →

Add simp lemmas for restricted product operations (#25462)

Estimated changes

Modified Mathlib/Topology/Algebra/RestrictedProduct.lean

added theorem RestrictedProduct.div_apply

added theorem RestrictedProduct.inv_apply

added theorem RestrictedProduct.mul_apply

added theorem RestrictedProduct.one_apply

added theorem RestrictedProduct.pow_apply

added theorem RestrictedProduct.smul_apply

added theorem RestrictedProduct.zpow_apply