Commit 2023-06-07 15:16 1ae835c7

View on Github →

feat: port noncomm_ring tactic (#4804) This aims to be a faithful implementation of mathlib3's noncomm_ring tactic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/SkewAdjoint.lean

Modified Mathlib/Analysis/NormedSpace/MStructure.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/NoncommRing.lean

added theorem Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul

added theorem Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul

Created test/NoncommRing.lean