Commit 2026-03-05 14:15 b630f5ad

View on Github →

feat(RatFunc): add notation for RatFunc (#36172) This PR adds notation for RatFunc. This syntax makes it fit nicely with preexisting notation for Polynomial, as you can see in this example:

Algebra.IsAlgebraic.rank_of_isFractionRing k[X] k⟮X⟯ K[X] K⟮X⟯

The parentheses are chosen to be like the one for IntermediateField.adjoin on purpose. I think this is nice because of consistency and it's easy to remember. However this means that there's a potential clash when using a variable X : F that one would like to adjoin to a field. See also related PR #35928 and discussion #mathlib4 > Notation for Algebra.adjoin @ 💬.

Estimated changes

modified def RatFunc.laurent
modified def RatFunc.laurentAux
modified def RatFunc.C
modified def RatFunc.X
modified theorem RatFunc.X_ne_zero
modified theorem RatFunc.algebraMap_C
modified theorem RatFunc.algebraMap_X
modified theorem RatFunc.algebraMap_comp_C
modified theorem RatFunc.algebraMap_eq_C
modified theorem RatFunc.denom_X
modified theorem RatFunc.eq_C_iff
modified def RatFunc.eval
modified theorem RatFunc.eval_add
modified theorem RatFunc.eval_mul
modified theorem RatFunc.num_X
modified theorem RatFunc.smul_eq_C_mul
modified theorem RatFunc.transcendental_X
modified theorem RatFunc.v_def
modified theorem RatFunc.algebraMap_ne_zero
modified theorem RatFunc.associated_num_inv
modified def RatFunc.coePolynomial
modified def RatFunc.denom
modified theorem RatFunc.denom_add_dvd
modified theorem RatFunc.denom_algebraMap
modified theorem RatFunc.denom_dvd
modified theorem RatFunc.denom_inv_dvd
modified theorem RatFunc.denom_mul_dvd
modified theorem RatFunc.denom_ne_zero
modified theorem RatFunc.denom_one
modified theorem RatFunc.denom_zero
modified theorem RatFunc.isCoprime_num_denom
modified def RatFunc.liftAlgHom
modified def RatFunc.liftRingHom
modified def RatFunc.mapAlgHom
modified theorem RatFunc.monic_denom
modified theorem RatFunc.mul_inv_cancel
modified def RatFunc.num
modified def RatFunc.numDenom
modified theorem RatFunc.num_denom_add
modified theorem RatFunc.num_denom_mul
modified theorem RatFunc.num_denom_neg
modified theorem RatFunc.num_div_denom
modified theorem RatFunc.num_dvd
modified theorem RatFunc.num_eq_zero_iff
modified theorem RatFunc.num_inv_dvd
modified theorem RatFunc.num_mul_dvd
modified theorem RatFunc.num_ne_zero
modified theorem RatFunc.num_one
modified theorem RatFunc.num_zero
modified theorem RatFunc.ofFractionRing_one
modified theorem RatFunc.ofFractionRing_zero
modified theorem RatFunc.smul_eq_C_smul
modified theorem RatFunc.toFractionRing_smul
modified theorem RatFunc.toFractionRing_inj
modified def RatFunc.intDegree
modified theorem RatFunc.intDegree_X
modified theorem RatFunc.intDegree_add
modified theorem RatFunc.intDegree_add_le
modified theorem RatFunc.intDegree_inv
modified theorem RatFunc.intDegree_mul
modified theorem RatFunc.intDegree_neg
modified theorem RatFunc.intDegree_one
modified theorem RatFunc.intDegree_zero
modified theorem RatFunc.adjoin_X
modified theorem RatFunc.minpolyX_aeval_X
modified theorem LaurentSeries.inducing_coe
modified theorem RatFunc.coe_X
modified theorem RatFunc.coe_coe