Theorem RatFunc.associated_num_inv

Modification history

2026-03-05 14:15
Mathlib/FieldTheory/RatFunc/Basic.lean
feat(RatFunc): add notation for RatFunc (#36172) …
Modified RatFunc.associated_num_invView on Github →
2026-01-22 14:48
Mathlib/FieldTheory/RatFunc/Basic.lean
feat(FieldTheory/RatFunc): Simple lemmas about num/denom and inv (#34211)
Added RatFunc.associated_num_invView on Github →