Implicit parameters in (Continuous)LinearMap.id

Stream: mathlib4

[Niels Voss]

I noticed that LinearMap.id has two explicit parameters while ContinuousLinearMap.id has all implicit parameters. Is there a reason for this difference?

[Eric Wieser]

docs#LinearMap.id does not have any explicit parameters.

[Niels Voss]

Sorry, I meant it the other way around. docs#ContinuousLinearMap.id has explicit parameters

[Eric Wieser]

I think docs#LinearMap.id is the odd one out here, docs#AlgHom.id and docs#AffineMap.id both also take explicit arguments.