[Merged by Bors] - feat(ring_theory/valuation/basic): add add_valuation.valuation #12914
Conversation
mariainesdff
commented
Mar 24, 2022
mariainesdff
commented
mariainesdff
added
the
awaiting-review
| @@ -492,6 +492,12 @@ variables {h0} {h1} {hadd} {hmul} {r : R} | |||
| @[simp] | |||
| theorem of_apply : (of f h0 h1 hadd hmul) r = f r := rfl | |||
|
|
|||
| /-- The `valuation` associated to an `add_valuation` (useful if the latter is constructed using | |||
| `add_valuation.of`). -/ | |||
| def valuation : valuation R (multiplicative (order_dual Γ₀)) := v | |||
There was a problem hiding this comment.
Does simps produce the lemma automatically?
There was a problem hiding this comment.
@[simps] gives me the error message Invalid simps attribute. The body is not a constructor application: v
There was a problem hiding this comment.
:( for simps, but thanks!
bors d+
|
✌️ mariainesdff can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
| `add_valuation.of`). -/ | ||
| def valuation : valuation R (multiplicative (order_dual Γ₀)) := v | ||
|
|
||
| @[simp] lemma valuation_apply (r : R) : v.valuation r = multiplicative.of_add (v r) := rfl |
There was a problem hiding this comment.
This statement looks wrong to me - this should be
| @[simp] lemma valuation_apply (r : R) : v.valuation r = multiplicative.of_add (v r) := rfl | |
| @[simp] lemma valuation_apply (r : R) : v.valuation r = multiplicative.of_add (order_dual.to_dual (v r)) := rfl |
(probably with line wrapping)
Let's fix this in a follow-up, so as not to interrupt the batch,
There was a problem hiding this comment.
Hmm I guess that makes sense, it's definitely what I meant. Why does rfl still work without the order_dual.to_dual?
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
YaelDillies
removed
the
awaiting-review
