linear_inv_right_inverse_from_iso

forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (f : forall (x : X), Y), forall (inv : forall (y : Y), X), forall (op_norm : Scalar), forall (inv_op_norm : Scalar), forall (iso_args : @LinearIsoArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f inv op_norm inv_op_norm), forall (y : Y), @Eq.{w} Y (f (@LinearInv.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f inv op_norm inv_op_norm y)) y

fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun f => fun inv => fun op_norm => fun inv_op_norm => fun iso_args => fun y => iso_args (@Eq.{w} Y (f (@LinearInv.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f inv op_norm inv_op_norm y)) y) (fun (forward_linear_arg : @LinearMapLawArgs.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f) => fun (inverse_linear_arg : @LinearMapLawArgs.{u,w,v} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm X xzero xadd xneg xsmul xnorm inv) => fun (forward_bound_arg : @OperatorNormBound.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f op_norm) => fun (inverse_bound_arg : @OperatorNormBound.{u,w,v} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm X xzero xadd xneg xsmul xnorm inv inv_op_norm) => fun (left_inverse_arg : forall (x : X), @Eq.{v} X (inv (f x)) x) => fun (right_inverse_arg : forall (y : Y), @Eq.{w} Y (f (inv y)) y) => right_inverse_arg y)