Commit 2025-10-27 12:10 a36ed518

View on Github →

feat: f r = r for f : ℝ →+* ℝ (#30486)

Estimated changes

added theorem Real.ringHom_apply