Commit 2026-01-22 14:48 cf30ec2d

View on Github →

feat(FieldTheory/RatFunc): Simple lemmas about num/denom and inv (#34211)

Estimated changes

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

added theorem RatFunc.associated_denom_inv

added theorem RatFunc.associated_num_inv

added theorem RatFunc.denom_inv_dvd

added theorem RatFunc.num_inv_dvd