Commit 2023-09-12 22:27 fd58eb4f

View on Github →

chore: use mk_iff more (#7105)

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

deleted theorem simply_connected_def

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

deleted theorem SimpleGraph.Walk.isCircuit_def

deleted theorem SimpleGraph.Walk.isTrail_def

Modified Mathlib/GroupTheory/Solvable.lean

deleted theorem isSolvable_def

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

deleted theorem IsPrimitiveRoot.iff_def