Theorem Real.ringHom_apply

Modification history

2026-03-21 05:31
Mathlib/Data/Real/CompleteField.lean
chore: deprecate `ConditionallyCompleteLinearOrderedField` (#35760) …
Modified Real.ringHom_applyView on Github →
2025-10-27 12:10
Mathlib/Data/Real/CompleteField.lean
feat: `f r = r` for `f : ℝ →+* ℝ` (#30486)
Added Real.ringHom_applyView on Github →