Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat: add Algebra.compHom and related lemma #18404

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
+85 −0
Open

feat: add Algebra.compHom and related lemma #18404

Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
f26d639
remove HasRingEquiv
yhtq Oct 29, 2024
9803b15
fix indent
yhtq Oct 29, 2024
a57db8b
fix style
yhtq Oct 29, 2024
4c2add7
fix style
yhtq Oct 29, 2024
0676cc5
reimplement
yhtq Oct 30, 2024
1885ef6
remove @[simp]
yhtq Oct 30, 2024
57db866
fix
yhtq Oct 30, 2024
91ca521
fix the defnition to ensure defeq
yhtq Oct 30, 2024
0835abb
add docstring
yhtq Oct 30, 2024
c5c8fe5
Update Mathlib/Algebra/Algebra/Defs.lean
yhtq Oct 30, 2024
b7f9f13
set docPrime linter
yhtq Oct 30, 2024
988c3ce
Merge branch 'galoisRamification' of https://github.com/leanprover-co…
yhtq Oct 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Mathlib/Algebra/Algebra/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,11 +175,13 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
smul_def' _ _ := rfl
toRingHom := i

/-- definition of smul of toAlgebra'-/
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
theorem RingHom.smul_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
(h : ∀ c x, i c * x = x * i c) (r: R) (s: S) :
let _ := RingHom.toAlgebra' i h
r • s = i r * s := rfl

/--definition of algebraMap of toAlgebra'-/
theorem RingHom.algebraMap_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
(h : ∀ c x, i c * x = x * i c) :
@algebraMap R S _ _ (i.toAlgebra' h) = i :=
Expand Down
Loading