Commit 2023-09-11 04:42 9893bbd2

View on Github →

chore: reduce imports to Data.Rat.Cast.CharZero (#7091) Removing further unnecessary imports on the path to major tactics.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Field/Power.lean

Created Mathlib/Algebra/GroupWithZero/Bitwise.lean

added theorem zpow_bit1'

added theorem zpow_bit1₀

Modified Mathlib/Algebra/GroupWithZero/Power.lean

deleted theorem map_zpow₀

deleted theorem zpow_bit1'

deleted theorem zpow_bit1₀

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

added theorem map_zpow₀

Modified Mathlib/Algebra/Order/Field/Power.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/Rat/Cast/CharZero.lean

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

Modified Mathlib/Tactic/NormNum/Ineq.lean