Commit 2025-06-26 23:40 ac6f8226

View on Github →

chore: golf using exact (#26397)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

modified theorem Submodule.mul_smul_mul_eq_smul_mul_smul

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/FieldTheory/Cardinality.lean

modified theorem Fintype.isPrimePow_card_of_field

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

Modified Mathlib/InformationTheory/Hamming.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/ModelTheory/Complexity.lean

Modified Mathlib/Order/Atoms/Finite.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Modified Mathlib/RingTheory/Valuation/AlgebraInstances.lean

Modified Mathlib/Tactic/ReduceModChar.lean

Modified Mathlib/Topology/Category/Stonean/Basic.lean