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

Porting note: was infer_instance #11187

Open
pitmonticone opened this issue Mar 5, 2024 · 0 comments
Open

Porting note: was infer_instance #11187

pitmonticone opened this issue Mar 5, 2024 · 0 comments
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.

Comments

@pitmonticone
Copy link
Collaborator

Classifies porting notes claiming:

was infer_instance

Examples

mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Lines 186 to 202 in 2a65c8d

instance forget₂Monoidal_faithful : Faithful (forget₂Monoidal R).toFunctor := by
dsimp [forget₂Monoidal]
-- Porting note: was `infer_instance`
exact FullSubcategory.faithful _
#align fgModule.forget₂_monoidal_faithful FGModuleCat.forget₂Monoidal_faithful
instance forget₂Monoidal_additive : (forget₂Monoidal R).toFunctor.Additive := by
dsimp [forget₂Monoidal]
-- Porting note: was `infer_instance`
exact Functor.fullSubcategoryInclusion_additive _
#align fgModule.forget₂_monoidal_additive FGModuleCat.forget₂Monoidal_additive
instance forget₂Monoidal_linear : (forget₂Monoidal R).toFunctor.Linear R := by
dsimp [forget₂Monoidal]
-- Porting note: was `infer_instance`
exact Functor.fullSubcategoryInclusionLinear _ _
#align fgModule.forget₂_monoidal_linear FGModuleCat.forget₂Monoidal_linear

@pitmonticone pitmonticone added the porting-notes Mathlib3 to Mathlib4 porting notes. label Mar 5, 2024
@pitmonticone pitmonticone mentioned this issue Mar 5, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Mar 5, 2024
@pitmonticone
chore: classify was infer_instance porting notes (#11188)
21e3d3b 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
kbuzzard pushed a commit that referenced this issue Mar 12, 2024
@pitmonticone @kbuzzard
chore: classify was infer_instance porting notes (#11188)
0fb8c5d 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@pitmonticone @dagurtomas
chore: classify was infer_instance porting notes (#11188)
34eaf7d 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
utensil pushed a commit that referenced this issue Mar 26, 2024
@pitmonticone @utensil
chore: classify was infer_instance porting notes (#11188)
30452cd 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
Louddy pushed a commit that referenced this issue Apr 15, 2024
@pitmonticone @Louddy
chore: classify was infer_instance porting notes (#11188)
20c3f40 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
callesonne pushed a commit that referenced this issue Apr 22, 2024
@pitmonticone @callesonne
chore: classify was infer_instance porting notes (#11188)
cfe2b10 
Classifying by adding issue number #11187 to porting notes claiming: 

> was `infer_instance`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@pitmonticone