Commit 2022-11-27 23:16 b7745675

View on Github →

feat(Algebra/Ring/Semiconj): port file (#751) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 porting notes:

Woot! mathport succeeded with no help!
I had to remove the simp attribute on two declarations because simpNF said so. I left porting notes.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Semiconj.lean

added theorem SemiconjBy.add_left

added theorem SemiconjBy.add_right

added theorem SemiconjBy.neg_left

added theorem SemiconjBy.neg_left_iff

added theorem SemiconjBy.neg_one_left

added theorem SemiconjBy.neg_one_right

added theorem SemiconjBy.neg_right

added theorem SemiconjBy.neg_right_iff

added theorem SemiconjBy.sub_left

added theorem SemiconjBy.sub_right