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] - fix(field_theory/intermediate_field): use a better algebra.smul
definition, and generalize
#10012
Conversation
…inition, and generalize Previously coe_smul was not true by `rfl`
7ac033b
to
3a28b09
Compare
instance module' {R} [semiring R] [has_scalar R K] [module R L] [is_scalar_tower R K L] : | ||
module R S := | ||
S.to_subalgebra.module' | ||
instance module : module K S := S.to_subalgebra.module |
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.
newline?
instance module : module K S := S.to_subalgebra.module | |
instance module : module K S := S.to_subalgebra.module |
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.
I'm copying
mathlib/src/algebra/algebra/subalgebra.lean
Lines 232 to 235 in d360f3c
instance module' [semiring R'] [has_scalar R' R] [module R' A] [is_scalar_tower R' R A] : | |
module R' S := | |
S.to_submodule.module' | |
instance : module R S := S.module' |
rw [trace_algebra_map, ← is_scalar_tower.algebra_map_smul K, (algebra.trace K K⟮x⟯).map_smul, | ||
smul_eq_mul, algebra.smul_def], | ||
apply_instance | ||
rw [trace_algebra_map, linear_map.map_smul_of_tower], |
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.
I'm not certain why this proof broke, but this new proof is better anyway.
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 🎉
bors merge
…inition, and generalize (#10012) Previously coe_smul was not true by `rfl`
Pull request successfully merged into master. Build succeeded: |
algebra.smul
definition, and generalizealgebra.smul
definition, and generalize
…inition, and generalize (#10012) Previously coe_smul was not true by `rfl`
Previously coe_smul was not true by
rfl