Commit 2024-08-16 13:44 9b07aee1

View on Github →

chore: Rename nonzero_of_invertible to Invertible.ne_zero (#15860) From LeanAPAP

Estimated changes

Modified Archive/Wiedijk100Theorems/SolutionOfCubic.lean

Modified Mathlib/Algebra/CharP/Invertible.lean

Modified Mathlib/Algebra/GroupWithZero/Invertible.lean

added theorem Invertible.ne_zero

deleted theorem nonzero_of_invertible

Modified Mathlib/Algebra/Ring/Invertible.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean

Modified Mathlib/Tactic/NormNum/Result.lean