-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(set_theory/surreal/dyadic): define add_monoid_hom structure on dyadic map #11052
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
otherwise lgtm!
src/set_theory/surreal/dyadic.lean
Outdated
... = a • pow_half b' + c • pow_half d' : add_comm _ _, | ||
end } | ||
|
||
lemma dyadic_map_apply (m : ℤ) (p : submonoid.powers (2 : ℤ)) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be a simp
lemma?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, I added it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It needed converting into simp normal form.
@[simp] lemma dyadic_map_apply (m : ℤ) (p : submonoid.powers (2 : ℤ)) :
dyadic_map (is_localization.mk' (localization (submonoid.powers 2)) m p) =
m • pow_half (submonoid.log p)
@@ -234,8 +236,8 @@ lemma pow_right_injective_iff_pow_injective {n : M} : | |||
function.injective (λ m : ℕ, n ^ m) ↔ function.injective (pow n) := | |||
subtype.coe_injective.of_comp_iff (pow n) | |||
|
|||
theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) (m : ℕ) : | |||
log (pow n m) = m := | |||
@[simp] theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we have simp
lemmas that prove h
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Otherwise LGTM
bors d+
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
h
isn't always true though. The closest we have are int.pow_right_injective
and nat.pow_right_injective
.
✌️ apurvnakade can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…yadic map (#11052) The proof is mechanical and mostly requires unraveling definitions. The above map cannot be extended to ring morphism as so far there's not multiplication structure on surreal numbers.
Pull request successfully merged into master. Build succeeded: |
The proof is mechanical and mostly requires unraveling definitions.
The above map cannot be extended to ring morphism as so far there's not multiplication structure on surreal numbers.